ext a
α : Type
inst : DecidableEq α
ys : List α
x : α
⊢ ↑(x :: ys).toFinset = {x} ∪ ↑ys.toFinset
case h
α : Type
inst : DecidableEq α
ys : List α
x a : α
⊢ a ∈ ↑(x :: ys).toFinset ↔ a ∈ {x} ∪ ↑ys.toFinset