no goals
α : Type u_1
β : Type ?u.110948
γ : Type ?u.110951
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
x : α
⊢ x ∈ insert a (insert a s) ↔ x ∈ insert a s
simp only [mem_insert, ←or_assoc, or_self_iff]