proposition: Lemma imset2_f (D : {pred aT}) (D2 : aT -> {pred aT2}) x x2 : x \in D -> x2 \in D2 x -> f2 x x2 \in [set f2 y y2 | y in D, y2 in D2 y].
proof: Proof. by move=> Dx Dx2; apply/imset2P; exists x x2. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)