proposition: Lemma morphim_sndX (H1: {group gT1}) (H2 : {set gT2}) : [morphism of fun x => x.2] @* setX H1 H2 = H2.
proof: Proof. apply/eqP; rewrite eqEsubset morphimE setTI /=. apply/andP; split; apply/subsetP=> x. by case/imsetP=> x0 /[1!inE] /andP[_ Hx2] ->. move=> Hx2; apply/imsetP; exists (1, x); last by []. by rewrite in_setX Hx2 andbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)