proposition: Lemma allpairs_uniq_dep f s t (st := [seq Tagged T y | x <- s, y <- t x]) : let g (p : {x : S & T x}) : R := f (tag p) (tagged p) in uniq s -> {in s, forall x, uniq (t x)} -> {in st &, injective g} -> uniq [seq f x y | x <- s, y <- t x].
proof: Proof. move=> g Us Ut; rewrite -(map_allpairs g (existT T)) => /map_inj_in_uniq->{f g}. elim: s Us => //= x s IHs /andP[s'x Us] in st Ut *; rewrite {st}cat_uniq. rewrite {}IHs {Us}// ?andbT => [|x1 s_s1]; last exact/Ut/mem_behead. have injT: injective (existT T x) by move=> y z /eqP; rewrite eq_Tagged => /eqP. rewrite (map_inj_in_uniq (in2W injT)) {injT}Ut ?mem_head // has_sym has_map. by apply: contra s'x => /hasP[y _ /allpairsPdep[z [_ [? _ /(congr1 tag)/=->]]]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)