simp only [if_pos c1]
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(if x ∈ visited then dft_aux g stack visited
        else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset