proposition: Lemma rex_pump_star_1: forall s1 s2 re, s1 \in re -> s2 \in r_star re -> s1 <> [] -> length s1 <= pumping_constant re -> RexPump (r_star re) (s1 ++ s2).
proof: Proof. intros. apply rex_pump_def with (x:=[]) (y:=s1) (z:=s2). * reflexivity. * intros N; subst. contradiction. * simpl. assumption. * intros. simpl. auto using pow_pump. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang