simp only [dft_aux]
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih :
  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
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g (dft_aux g (x :: stack) visited) ⊆ ↑(dft_aux g (x :: stack) visited).toFinset
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih :
  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
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g
      (if x ∈ visited then dft_aux g stack visited else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
    ↑(if x ∈ visited then dft_aux g stack visited
        else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset