induction stack, visited using dft_aux.induct g
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack visited : List Node
⊢ stack ⊆ dft_aux g stack visited
case case1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited✝ : List Node
⊢ [] ⊆ dft_aux g [] visited✝

case case2
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited✝ : List Node
x✝ : Node
xs✝ : List Node
h✝ : x✝ ∈ visited✝
ih1✝ : xs✝ ⊆ dft_aux g xs✝ visited✝
⊢ x✝ :: xs✝ ⊆ dft_aux g (x✝ :: xs✝) visited✝

case case3
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited✝ : List Node
x✝ : Node
xs✝ : List Node
h✝ : x✝ ∉ visited✝
ih1✝ : direct_succ_list g x✝ ++ xs✝ ⊆ dft_aux g (direct_succ_list g x✝ ++ xs✝) (x✝ :: visited✝)
⊢ x✝ :: xs✝ ⊆ dft_aux g (x✝ :: xs✝) visited✝