proposition: Lemma rex_pump_star_2: forall re s1 s2, RexPump re s1 -> s2 \in r_star re -> RexPump (r_star re) (s1 ++ s2).
proof: Proof. intros. inversion H; subst; clear H. apply rex_pump_def with (x:=x)(y:=y)(z:=z++s2); simpl; auto. * repeat rewrite <- app_assoc; reflexivity. * intros. apply accept_star_cons with (s1:=x ++ pow y m ++ z) (s2:=s2); auto. repeat rewrite app_assoc. reflexivity. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang