proposition: Lemma r_pow_to_pow: forall n s r, s \in r_pow r n -> Pow (Accept r) n s.
proof: Proof. induction n; intros; simpl in *. - inversion H; subst. constructor. - inversion H; subst; clear H. apply IHn in H3. eapply pow_cons; eauto. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang