case _ visited x stack c1 ih =>
  simp only [dft_aux]
  simp only [if_pos c1]
  apply extracted_1 (dft_aux g stack visited) visited stack x ih c1
  exact visited_subset_dft_aux g stack visited
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : stack ⊆ dft_aux g stack visited
⊢ x :: stack ⊆ dft_aux g (x :: stack) visited
no goals