have s1 : (dft_aux g stack []).toFinset.toSet = reachable_from_list g (dft_aux g stack []) :=
by
  apply list_direct_succ_set_closed_reachable_from_list g (dft_aux g stack [])
  exact list_direct_succ_set_closed_dft_aux g stack
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ reachable_from_list g stack ⊆ ↑(dft_aux g stack []).toFinset
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 ⊆ ↑(dft_aux g stack []).toFinset