proposition: Lemma regularU (L1 L2 : lang char) : regular L1 -> regular L2 -> regular (fun x => L1 x \/ L2 x).
proof: Proof. move => [A1 acc_L1] [A2 acc_L2]. exists (dfa_op orb A1 A2) => x. by rewrite dfa_op_correct -(rwP orP) -acc_L1 -acc_L2. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)