simp only [Set.subset_def]
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
⊢ reachable_from_list g (xs ++ ys) ⊆ reachable_from_list g xs ∪ reachable_from_list g ys
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
⊢ ∀ x ∈ reachable_from_list g (xs ++ ys), x ∈ reachable_from_list g xs ∪ reachable_from_list g ys