no goals
α : Type u_1
β : Type ?u.216030
γ : Type ?u.216033
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b : α
s : Finset α
a : α
h : ¬a ∈ s
⊢ erase (cons a s h) a = s
rw [cons_eq_insert, erase_insert_eq_erase, erase_eq_of_not_mem h]