simp only [dft_aux]
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∉ visited
ih :
  dft_aux g (direct_succ_list g x ++ xs ++ ys) (x :: visited) =
    dft_aux g ys (dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
⊢ dft_aux g (x :: (xs ++ ys)) visited = dft_aux g (direct_succ_list g x ++ (xs ++ ys)) (x :: visited)
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∉ visited
ih :
  dft_aux g (direct_succ_list g x ++ xs ++ ys) (x :: visited) =
    dft_aux g ys (dft_aux g (direct_succ_list g x ++ xs) (x :: visited))
⊢ (if x ∈ visited then dft_aux g (xs ++ ys) visited
    else dft_aux g (direct_succ_list g x ++ (xs ++ ys)) (x :: visited)) =
    dft_aux g (direct_succ_list g x ++ (xs ++ ys)) (x :: visited)