proposition: Lemma actsU : [acts A, on S :|: T | to].
proof: Proof. by apply: subset_trans astabsU; rewrite subsetI AactS. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)