proposition: Lemma actsP A S : reflect {acts A, on S | to} [acts A, on S | to].
proof: Proof. apply: (iffP idP) => [nSA x|nSA]; first exact: acts_act. by apply/subsetP=> a Aa /[!inE]; apply/subsetP=> x; rewrite inE nSA. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)