no goals
α : Type u_1
β : Type ?u.210946
γ : Type ?u.210949
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b✝ a b : α
s : Finset α
ha : ¬a ∈ s
hb : a ≠ b
⊢ erase (cons a s ha) b = cons a (erase s b) (_ : a ∈ erase s b → False)
simp only [cons_eq_insert, erase_insert_of_ne hb]