proposition: Lemma as_lang_rw: forall r, Equiv (Accept r) (as_lang r).
proof: Proof. induction r; simpl. - rewrite r_void_rw. reflexivity. - rewrite r_nil_rw. reflexivity. - rewrite r_char_rw. reflexivity. - rewrite <- IHr1. rewrite <- IHr2. rewrite r_app_rw. reflexivity. - rewrite <- IHr2. rewrite <- IHr1. rewrite r_union_rw. reflexivity. - rewrite <- IHr. rewrite r_star_rw. reflexivity. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang