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