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