simp only [list_direct_succ_set] at h1
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : list_direct_succ_set g xs ⊆ ↑xs.toFinset
⊢ reachable_from_list g xs ⊆ ↑xs.toFinset
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : {y | ∃ x ∈ xs, ∃ ys, y ∈ ys ∧ (x, ys) ∈ g} ⊆ ↑xs.toFinset
⊢ reachable_from_list g xs ⊆ ↑xs.toFinset