no goals
α : Type u_1
β : Type ?u.469108
γ : Type ?u.469111
inst✝ : DecidableEq α
l l' : List α
a✝ : α
a b : List α
⊢ toFinset a = toFinset b ↔ ∀ (x : α), x ∈ a ↔ x ∈ b
simp only [Finset.ext_iff, mem_toFinset]