proposition: Lemma setactU S T a : to^* (S :|: T) a = to^* S a :|: to^* T a.
proof: Proof. by rewrite /setact imsetU //; 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)