simp only [Set.subset_def]
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
⊢ reachable_from_list g xs ⊆ ↑xs.toFinset
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : ∀ (a x : α), x ∈ xs → ∀ (x_1 : List α), a ∈ x_1 → (x, x_1) ∈ g → a ∈ xs
⊢ ∀ x ∈ reachable_from_list g xs, x ∈ ↑xs.toFinset