Theorem: reachable_from_list_of_cons (FOL/Parsing/DFT.lean)

State before:
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
Tactic:
simp only [← reachable_from_list_of_append]
State after:
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)

State before:
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)
Tactic:
simp
State after:
no goals