proposition: Lemma pow_pump: forall m s1 s2 re, s1 \in re -> s2 \in r_star re -> pow s1 m ++ s2 \in r_star re.
proof: Proof. induction m; intros; simpl. { assumption. } apply accept_star_cons with (s1:=s1) (s2:=pow s1 m ++ s2); auto. rewrite app_assoc. reflexivity. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang