proposition: Lemma stack_visit x : x \notin seen e -> stack (visit x e) = x |: stack e.
proof: Proof. move=> xNseen; apply/setP=> y; rewrite !inE/= ffunE/= ?serialE// seen_visit. have [->|neq_yx]//= := altP eqP; first by rewrite cardsU1 xNseen ltnS ?leqnn. by rewrite num_lt_card// subsetUr. Qed.
imports: mathcomp(all_ssreflect) bigmin extra