induction stack, visited using dft_aux.induct g
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack visited : List Node
h1 : list_direct_succ_set g visited ⊆ ↑stack.toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g (dft_aux g stack visited) ⊆ ↑(dft_aux g stack visited).toFinset
case case1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited✝ : List Node
h1 : list_direct_succ_set g visited✝ ⊆ ↑[].toFinset ∪ ↑visited✝.toFinset
⊢ list_direct_succ_set g (dft_aux g [] visited✝) ⊆ ↑(dft_aux 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✝ :
  list_direct_succ_set g visited✝ ⊆ ↑xs✝.toFinset ∪ ↑visited✝.toFinset →
    list_direct_succ_set g (dft_aux g xs✝ visited✝) ⊆ ↑(dft_aux g xs✝ visited✝).toFinset
h1 : list_direct_succ_set g visited✝ ⊆ ↑(x✝ :: xs✝).toFinset ∪ ↑visited✝.toFinset
⊢ list_direct_succ_set g (dft_aux g (x✝ :: xs✝) visited✝) ⊆ ↑(dft_aux 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✝ :
  list_direct_succ_set g (x✝ :: visited✝) ⊆ ↑(direct_succ_list g x✝ ++ xs✝).toFinset ∪ ↑(x✝ :: visited✝).toFinset →
    list_direct_succ_set g (dft_aux g (direct_succ_list g x✝ ++ xs✝) (x✝ :: visited✝)) ⊆
      ↑(dft_aux g (direct_succ_list g x✝ ++ xs✝) (x✝ :: visited✝)).toFinset
h1 : list_direct_succ_set g visited✝ ⊆ ↑(x✝ :: xs✝).toFinset ∪ ↑visited✝.toFinset
⊢ list_direct_succ_set g (dft_aux g (x✝ :: xs✝) visited✝) ⊆ ↑(dft_aux g (x✝ :: xs✝) visited✝).toFinset