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