proposition: Lemma perm_allpairs_consr f s y0 t : perm_eql [seq f x y | x <- s, y <- y0 x :: t x] ([seq f x (y0 x) | x <- s] ++ [seq f x y | x <- s, y <- t x]).
proof: Proof. by apply/permPl; rewrite (perm_allpairs_catr _ _ (fun=> [:: _])) allpairs1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)