simp only [list_cons_to_set_union]
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ ↑(x :: ys).toFinset ∪ ↑xs.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ {x} ∪ ↑ys.toFinset ∪ ↑xs.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset