proposition: Lemma mem_allpairs_catr f s y0 t : [seq f x y | x <- s, y <- y0 x ++ t x] =i [seq f x y | x <- s, y <- y0 x] ++ [seq f x y | x <- s, y <- t x].
proof: Proof. exact/perm_mem/permPl/perm_allpairs_catr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)