proposition: Lemma allpairs_cat f s1 s2 t : [seq f x y | x <- s1 ++ s2, y <- t x] = [seq f x y | x <- s1, y <- t x] ++ [seq f x y | x <- s2, y <- t x].
proof: Proof. by rewrite map_cat flatten_cat. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)