apply reachable_from_list_mono g stack (dft_aux g stack [])
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset = reachable_from_list g (dft_aux g stack [])
⊢ reachable_from_list g stack ⊆ reachable_from_list g (dft_aux g stack [])
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset = reachable_from_list g (dft_aux g stack [])
⊢ stack ⊆ dft_aux g stack []