proposition: Lemma l2_is_reg: Regular Examples.L2.
proof: Proof. apply regular_def with (r:= r_any ;; r_any). unfold Equiv, Examples.L2; split; intros. - inversion H; subst. apply accept_any_inv in H2. apply accept_any_inv in H3. destruct H2 as (c1, ?). destruct H3 as (c2, ?). subst. reflexivity. - destruct w. { inversion H. } inversion H; subst; clear H. destruct w. { inversion H1. } inversion H1; subst; clear H1. destruct w. { simpl. apply accept_any_cons. apply accept_any. } inversion H0. Qed.
imports: Coq.Strings.Ascii Coq.Lists.List Coq.Strings.Ascii Coq.Arith.PeanoNat Coq.micromega.Lia Turing.Lang Turing.Regex Turing.Util