proposition: Lemma acts_gen A S : S \subset R -> [acts A, on S | to] -> [acts A, on <<S>> | to].
proof: Proof. move=> sSR actsA; apply: {A}subset_trans actsA _. apply/subsetP=> a nSa; have Da := astabs_dom nSa; rewrite !inE Da. apply: subset_trans (_ : <<S>> \subset actm to a @*^-1 <<S>>) _. rewrite gen_subG subsetI sSR; apply/subsetP=> x Sx. by rewrite inE /= actmE ?mem_gen // astabs_act. by apply/subsetP=> x /[!inE]; case/andP=> Rx; rewrite /= actmE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)