proposition: Lemma tuto_sum_enum_uniq : forall T1 T2, uniq (sum_enum T1 T2).
proof: Proof. move=> T1 T2. Search _ cat uniq. rewrite cat_uniq. Search _ uniq map. rewrite !map_inj_uniq. Search _ uniq Finite.enum. Search _ Finite.enum. + rewrite -!enumT. Search _ (enum _) uniq. rewrite !enum_uniq /= andbT. apply/hasP => [[u]]. case/mapP=> x hx -> /=. case/mapP. done. + by move=> x y []. + by move=> x y []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)