proposition: Lemma tuto_sum_enum_uniq_clean : forall T1 T2, uniq (sum_enum T1 T2).
proof: Proof. move=> T1 T2. rewrite cat_uniq -!enumT !(enum_uniq, map_inj_uniq); try by move=> ? ? []. by rewrite andbT; apply/hasP=> [[u]]; case/mapP=> x _ ->; case/mapP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)