induction stack, visited using dft_aux.induct g
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack visited : List Node
⊢ ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
case case1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited✝ : List Node
⊢ ↑(dft_aux g [] visited✝).toFinset ⊆ reachable_from_list g [] ∪ ↑visited✝.toFinset

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

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