proposition: Lemma r_pow_rw: forall r n, Equiv (Accept (r_pow r n)) (Pow (Accept r) n).
proof: Proof. induction n; intros. - split; simpl; intros. + inversion H; subst; clear H. apply pow_nil. + inversion H; subst; clear H. apply accept_nil. - split; simpl; intros. + inversion H; subst; clear H. apply IHn in H3. apply pow_cons_eq; auto. + inversion H; subst; clear H. apply IHn in H1. apply accept_app_eq; auto. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang