simp only [if_neg c1]
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 (x :: visited) ⊆ ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset →
    list_direct_succ_set g (dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
      ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: 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
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 (x :: visited) ⊆ ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset →
    list_direct_succ_set g (dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
      ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g (dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
    ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset