proposition: Lemma perm_allpairs_catr f s t1 t2 : perm_eql [seq f x y | x <- s, y <- t1 x ++ t2 x] ([seq f x y | x <- s, y <- t1 x] ++ [seq f x y | x <- s, y <- t2 x]).
proof: Proof. apply/permPl; rewrite perm_sym; elim: s => //= x s ihs. by rewrite perm_catACA perm_cat ?map_cat. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)