proposition: Lemma regular_bigU (T : eqType) (L : T -> lang char) (s : seq T) : (forall a, a \in s -> regular (L a)) -> regular (fun x => exists2 a, a \in s & L a x).
proof: Proof. elim: s => //. - move => _. apply: regular_ext regular0 _. by split => // [[a]]. - move => a s IH /forall_consT [H1 H2]. pose L' := (fun x => L a x \/ (fun x : word => exists2 a : T, a \in s & L a x) x). apply: (regular_ext (L2 := L')); first by apply: regularU => //; exact: IH. move => x. rewrite /L'. exact: exists_cons. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)