proposition: Lemma perm_allpairs f s1 t1 s2 t2 : perm_eq s1 s2 -> perm_eq t1 t2 -> perm_eq [seq f x y | x <- s1, y <- t1] [seq f x y | x <- s2, y <- t2].
proof: Proof. by move=> perm_s perm_t; apply: perm_allpairs_dep. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)