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

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack visited : List Node
x : Node
h1 : x ∈ visited
⊢ dft_aux g (x :: stack) visited = dft_aux g stack visited
Tactic:
simp only [dft_aux]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack visited : List Node
x : Node
h1 : x ∈ visited
⊢ (if x ∈ visited then dft_aux g stack visited else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) =
    dft_aux g stack visited

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack visited : List Node
x : Node
h1 : x ∈ visited
⊢ (if x ∈ visited then dft_aux g stack visited else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) =
    dft_aux g stack visited
Tactic:
simp only [if_pos h1]
State after:
no goals