proposition: Lemma astabs_subact S : 'N(S | subaction) = subact_dom :&: 'N(val @: S | to).
proof: Proof. apply/setP=> a; rewrite inE in_setI; apply: andb_id2l => sDa. have [Da _] := setIP sDa; rewrite !inE Da. apply/subsetP/subsetP=> [nSa _ /imsetP[x Sx ->] | nSa x Sx] /[!inE]. by have /[1!inE]/(imset_f val) := nSa x Sx; rewrite val_subact sDa. have /[1!inE]/imsetP[y Sy def_y] := nSa _ (imset_f val Sx). by rewrite ((_ a =P y) _) // -val_eqE val_subact sDa def_y. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)