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