proposition: Lemma setactI S T a : to^* (S :&: T) a = to^* S a :&: to^* T a.
proof: Proof. by rewrite /setact imsetI //; apply: in2W; apply: act_inj. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype div) mathcomp(finset fingroup perm morphism action)