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 : x :: visited ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
⊢ visited ⊆ if x ∈ visited then dft_aux g stack visited else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih : x :: visited ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)
⊢ visited ⊆ dft_aux g (direct_succ_list g x ++ stack) (x :: visited)