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

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ list_direct_succ_list g (x :: xs) = direct_succ_list g x ++ list_direct_succ_list g xs
Tactic:
simp only [list_direct_succ_list]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ (List.map (fun x => direct_succ_list g x) (x :: xs)).join =
    direct_succ_list g x ++ (List.map (fun x => direct_succ_list g x) xs).join

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ (List.map (fun x => direct_succ_list g x) (x :: xs)).join =
    direct_succ_list g x ++ (List.map (fun x => direct_succ_list g x) xs).join
Tactic:
simp
State after:
no goals