proposition: Lemma gactsI (N1 N2 : {set rT}) : [acts A, on N1 | to] -> [acts A, on N2 | to] -> [acts A, on N1 :&: N2 | to].
proof: Proof. move=> aAN1 aAN2. apply/subsetP=> x Ax; rewrite !inE Ax /=; apply/subsetP=> y Ny /[1!inE]. case/setIP: Ny=> N1y N2y; rewrite inE ?astabs_act ?N1y ?N2y //. - by move/subsetP: aAN2; move/(_ x Ax). - by move/subsetP: aAN1; move/(_ x Ax). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action gseries)