proposition: Lemma accept_pow: forall s r i, s \in r -> Util.pow s i \in r_star r.
proof: Proof. induction i; intros. - apply accept_star_nil. - simpl. apply accept_star_cons with (s1:=s) (s2:=pow s i). + assumption. + auto. + reflexivity. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang