simp only [dft_aux]
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)
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
ys visited : List Node
⊢ dft_aux g ([] ++ ys) visited = dft_aux g ys visited