case a
α : Type u_1
β : Type ?u.13019
a✝ : α
⊢ a✝ ∈ ↑eraseNone {none} ↔ a✝ ∈ ∅
α : Type u_1
β : Type ?u.13019
⊢ ↑eraseNone {none} = ∅
ext
no goals
case a
α : Type u_1
β : Type ?u.13019
a✝ : α
⊢ a✝ ∈ ↑eraseNone {none} ↔ a✝ ∈ ∅
simp