proposition: Lemma imsetI (A B : {set aT}) : {in A & B, injective f} -> f @: (A :&: B) = f @: A :&: f @: B.
proof: Proof. move=> injf; apply/eqP; rewrite eqEsubset subsetI. rewrite 2?imsetS (andTb, subsetIl, subsetIr) //=. apply/subsetP=> _ /setIP[/imsetP[x Ax ->] /imsetP[z Bz /injf eqxz]]. by rewrite imset_f // inE Ax eqxz. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)