proposition: Lemma allpairsPdep R (f : forall x, T x -> R) s t (z : R) : reflect (exists x y, [/\ x \in s, y \in t x & z = f x y]) (z \in [seq f x y | x <- s, y <- t x]).
proof: Proof. apply: (iffP flatten_mapP); first by case=> x sx /mapP[y ty ->]; exists x, y. by case=> x [y [sx ty ->]]; exists x; last apply: map_f. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)