proposition: Lemma dfs_uniq (v : seq T) x n : uniq v -> uniq (dfs g n v x).
proof: Proof. elim: n v x => [|/= n IHn] v x uniq_v ; first by rewrite /= if_same. have [//|xNv] := boolP (x \in v). have: uniq (x::v) by rewrite /= xNv. elim: (g x) (x::v) => //= => {v x uniq_v xNv} y gx IHgx v uniq_v. exact/IHgx/IHn. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry) GraphTheory(preliminaries digraph sgraph) GraphTheory(hmap_ops embedding)