proposition: Lemma val_subact u a : val (subact u a) = if a \in subact_dom then to (val u) a else val u.
proof: Proof. by rewrite /subact -if_neg; case: insubP => [Na|] -> //=; rewrite SubK => ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)