proposition: Lemma l1_is_reg: Regular Examples.L1.
proof: Proof. apply regular_def with (r:= r_star r_any ;; "a"). unfold Examples.L1. rewrite r_app_rw. rewrite r_char_rw. rewrite r_star_rw. rewrite r_any_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