simp only [s1]
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
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 [])