induction xs, zs using dft_aux.induct g
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys zs : List Node
⊢ dft_aux g (xs ++ ys) zs = dft_aux g ys (dft_aux g xs zs)
case case1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited✝ : List Node
⊢ dft_aux g ([] ++ ys) visited✝ = dft_aux g ys (dft_aux g [] visited✝)

case case2
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited✝ : List Node
x✝ : Node
xs✝ : List Node
h✝ : x✝ ∈ visited✝
ih1✝ : 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 ys (dft_aux g (x✝ :: xs✝) visited✝)

case case3
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited✝ : List Node
x✝ : Node
xs✝ : List Node
h✝ : x✝ ∉ visited✝
ih1✝ :
  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 ys (dft_aux g (x✝ :: xs✝) visited✝)