simp
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
x : Node
xs : List Node
c1 : x ∈ visited
ih : dft_aux g (xs ++ ys) visited = dft_aux g ys (dft_aux g xs visited)
⊢ dft_aux g (x :: xs ++ ys) visited = dft_aux g (xs ++ ys) 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 (xs ++ ys) visited = dft_aux g ys (dft_aux g xs visited)
⊢ dft_aux g (x :: (xs ++ ys)) visited = dft_aux g (xs ++ ys) visited