proposition: Lemma l1_l3: Regular (Lang.Union Examples.L1 Examples.L3).
proof: Proof. apply union_regular. - apply l1_is_reg. - apply l3_is_reg. Qed.
imports: Coq.Strings.Ascii Coq.Lists.List Coq.Strings.Ascii Coq.Arith.PeanoNat Coq.micromega.Lia Turing.Lang Turing.Regex Turing.Util