proposition: Lemma imset2S (A B : {pred aT}) (A2 B2 : {pred aT2}) : A \subset B -> A2 \subset B2 -> f2 @2: (A, A2) \subset f2 @2: (B, B2).
proof: Proof. by move=> /(imset2Sl B2) sBA /(imset2Sr A)/subset_trans->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)