proposition: Lemma astab_subact S : 'C(S | subaction) = subact_dom :&: 'C(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=> [cSa _ /imsetP[x Sx ->] | cSa x Sx] /[!inE]. by have:= cSa x Sx; rewrite inE -val_eqE val_subact sDa. by have:= cSa _ (imset_f val Sx); rewrite inE -val_eqE val_subact sDa. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)