proposition: Corollary vec_lang_regular n s : regular (@vec_lang n s).
proof: Proof. apply/nfa_regular. exists (nfa_of_form n s) => x. apply: rwP. exact: nfa_of_form_correct. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)