apply base_of_reachable_from_list_is_subset_of_reachable_from_list
case a
α : Type
inst✝ : DecidableEq α
g : Graph α
xs : List α
h1 : list_direct_succ_set g xs ⊆ ↑xs.toFinset
⊢ ↑xs.toFinset ⊆ reachable_from_list g xs
no goals