simp only [← reachable_from_list_of_append]
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
ys : List Node
⊢ reachable_from_list g (x :: ys) = reachable_from_list g [x] ∪ reachable_from_list g ys
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
ys : List Node
⊢ reachable_from_list g (x :: ys) = reachable_from_list g ([x] ++ ys)