proposition: Lemma allpairs_uniq f s t (st := [seq (x, y) | x <- s, y <- t]) : uniq s -> uniq t -> {in st &, injective (uncurry f)} -> uniq [seq f x y | x <- s, y <- t].
proof: Proof. move=> Us Ut inj_f; rewrite -(map_allpairs (uncurry f) (@pair S T)) -/st. rewrite map_inj_in_uniq // allpairs_uniq_dep {Us Ut st inj_f}//. by apply: in2W => -[x1 y1] [x2 y2] /= [-> ->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)