proposition: Lemma r_star_rw: forall r, Equiv (Accept (r_star r)) (Lang.Star (Accept r)).
proof: Proof. split; intros. - apply r_star_to_pow in H. destruct H as (n, Hp). apply pow_to_star with (n:=n). apply r_pow_to_pow; assumption. - destruct H as (n, Hp). induction Hp. { apply accept_star_nil. } eapply accept_star_cons; eauto. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang