case _ visited =>
  simp only [dft_aux]
  simp
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ ↑(dft_aux g [] visited).toFinset ⊆ reachable_from_list g [] ∪ ↑visited.toFinset
no goals