simp only [Set.subset_def]
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
⊢ ↑xs.toFinset ⊆ reachable_from_list g xs
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
⊢ ∀ x ∈ ↑xs.toFinset, x ∈ reachable_from_list g xs