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