simp only [dft_aux]
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
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