proposition: Lemma ker_actperm : 'ker actperm = 'C(setT | to).
proof: Proof. congr (_ :&: _); apply/setP=> a /[!inE]/=. apply/eqP/subsetP=> [a1 x _ | a1]; first by rewrite inE -actpermE a1 perm1. by apply/permP=> x; apply/eqP; have:= a1 x; rewrite !inE actpermE perm1 => ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)