exact Set.eq_of_subset_of_subset s1 s2
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset ⊆ reachable_from_list g stack
s2 : reachable_from_list g stack ⊆ ↑(dft_aux g stack []).toFinset
⊢ ↑(dft_aux g stack []).toFinset = reachable_from_list g stack
no goals