proposition: Lemma allpairs_f_dep f s t x y : x \in s -> y \in t x -> f x y \in [seq f x y | x <- s, y <- t x].
proof: Proof. by move=> sx ty; apply/allpairsPdep; exists x, y. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)