simp only [dft_aux]
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
h1 : list_direct_succ_set g visited ⊆ {a | a ∈ visited}
⊢ list_direct_succ_set g (dft_aux g [] visited) ⊆ ↑(dft_aux g [] visited).toFinset
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
h1 : list_direct_succ_set g visited ⊆ {a | a ∈ visited}
⊢ list_direct_succ_set g visited ⊆ ↑visited.toFinset