simp only [list_cons_to_set_union] at h1
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : S ⊆ ↑(x :: zs).toFinset ∪ ↑ys.toFinset
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ↑(x :: ys).toFinset
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : S ⊆ {x} ∪ ↑zs.toFinset ∪ ↑ys.toFinset
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ↑(x :: ys).toFinset