proposition: Corollary mso_regular (char: finType) s : regular (@mso_lang char s).
proof: Proof. apply: regular_ext (mso_preim s). exact: preim_regular (@vec_of_hom _) (vec_lang_regular _ _). Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)