proposition: Lemma mem_allpairs f s1 t1 s2 t2 : s1 =i s2 -> t1 =i t2 -> [seq f x y | x <- s1, y <- t1] =i [seq f x y | x <- s2, y <- t2].
proof: Proof. by move=> eq_s eq_t; apply: mem_allpairs_dep. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)