proposition: Lemma morph_afix : h @: 'Fix_(S | to1)(A) = 'Fix_(h @: S | to2)(f @* A).
proof: Proof. apply/setP=> hu; apply/imsetP/setIP=> [[u /setIP[Su cAu] ->]|]. split; first by rewrite imset_f. by apply/afixP=> _ /morphimP[x D1x Ax ->]; rewrite -hfJ ?(afixP cAu). case=> /imsetP[u Su ->] /afixP c_hu_fA; exists u; rewrite // inE Su. apply/afixP=> x Ax; have Dx := subsetP sAD1 x Ax. by apply: injh; rewrite ?actsDR ?(subsetP sSR) ?hfJ // c_hu_fA ?mem_morphim. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)