proposition: Lemma imset2Sr (A B : {pred aT2}) (C : {pred aT}) : A \subset B -> f2 @2: (C, A) \subset f2 @2: (C, B).
proof: Proof. move=> sAB; apply/subsetP=> _ /imset2P[x y Ax Cy ->]. by apply/imset2P; exists x y; rewrite ?(subsetP sAB). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)