no goals
α : Type u_1
β : Type ?u.209336
γ : Type ?u.209339
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b : α
s : Finset α
a x : α
⊢ x ∈ erase (insert a s) a ↔ x ∈ erase s a
simp (config := { contextual := true }) only [mem_erase, mem_insert, and_congr_right_iff,
  false_or_iff, iff_self_iff, imp_true_iff]