apply list_direct_succ_set_closed_dft_aux_aux
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ list_direct_succ_set g (dft_aux g stack []) ⊆ ↑(dft_aux g stack []).toFinset
case h1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ list_direct_succ_set g [] ⊆ ↑stack.toFinset ∪ ↑[].toFinset