have s1 : (dft_aux g stack []).toFinset.toSet ⊆ reachable_from_list g stack ∪ [].toFinset.toSet := dft_aux_is_subset_of_reachable_from_list_and_visited g stack []
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ ↑(dft_aux g stack []).toFinset = reachable_from_list g stack
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset ⊆ reachable_from_list g stack ∪ ↑[].toFinset
⊢ ↑(dft_aux g stack []).toFinset = reachable_from_list g stack