apply Set.union_subset
case sr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ {x} ∪ ↑ys.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset
case sr.sr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ {x} ⊆ ↑ys.toFinset ∪ ↑xs.toFinset

case sr.tr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ ↑ys.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset