exact Set.mem_of_subset_of_mem s1 left
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x hd : Node
tl : List Node
ih : x ∈ reachable_from_list g (list_direct_succ_list g tl) → x ∈ reachable_from_list g tl
left : x ∈ reachable_from_list g (direct_succ_list g hd)
s1 : reachable_from_list g (direct_succ_list g hd) ⊆ reachable_from_list g [hd]
⊢ x ∈ reachable_from_list g [hd]
no goals