proposition: Lemma prod_enum_uniq : forall T1 T2, uniq (tuto_prod_enum T1 T2).
proof: Proof. move=> T1 T2; rewrite /tuto_prod_enum; move: (enum_uniq T1) (enum_uniq T2). elim: (enum T1) (enum T2)=> [|x1 l1 ihl1] l2 //=; case/andP=> hx1 uniq_l1 uniq_l2. rewrite cat_uniq ihl1 // andbT map_inj_uniq; last by move=> x y []. rewrite uniq_l2 /=; apply/hasP=> [[u]] /= h1; case/mapP=> y l2y e. move: h1; rewrite e; elim: l1 hx1 {uniq_l1 ihl1} => [|x3 l3 ihl3 ] //=. rewrite in_cons negb_or; case/andP=> h1 h2. rewrite mem_cat; case/orP; last by apply: ihl3. by case/mapP=> y' _ []; move/eqP; move/negPf: h1 => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)