proposition: Lemma acts_act A S : [acts A, on S | to] -> {acts A, on S | to}.
proof: Proof. by move=> nAS a Aa x; rewrite astabs_act ?(subsetP nAS). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)