proposition: Lemma l3_is_reg: Regular Examples.L3.
proof: Proof. unfold Examples.L3. apply regular_def with (r:="a" ;; r_star r_any ;; "b"). repeat rewrite r_app_rw. rewrite r_star_rw. rewrite r_any_rw. repeat rewrite r_char_rw. rewrite star_any_rw. reflexivity. Qed.
imports: Coq.Strings.Ascii Coq.Lists.List Coq.Strings.Ascii Coq.Arith.PeanoNat Coq.micromega.Lia Turing.Lang Turing.Regex Turing.Util