ext
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
⊢ A \ insert v B = erase (A \ B) v
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
⊢ a✝ ∈ A \ insert v B ↔ a✝ ∈ erase (A \ B) v