proposition: Lemma sub_act_proof u Na : sP (to (val u) (val Na)).
proof: Proof. by case: Na => a /= /(astabs_act (val u)); rewrite !inE valP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)