simp only [dft_aux]
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ visited ⊆ dft_aux g [] visited
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ visited ⊆ visited