proposition: Lemma mem_allpairs_dep f s1 t1 s2 t2 : s1 =i s2 -> {in s1, forall x, t1 x =i t2 x} -> [seq f x y | x <- s1, y <- t1 x] =i [seq f x y | x <- s2, y <- t2 x].
proof: Proof. move=> eq_s eq_t z; apply/allpairsPdep/allpairsPdep=> -[x [y [sx ty ->]]]; by exists x, y; rewrite -eq_s in sx *; rewrite eq_t in ty *. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)