fact: Fixpoint nfa_of_form n s {struct s} : nfa (vec n) := match s with | Incl X Y => nfa_for_incl n X Y | Less X Y => nfa_for_ltn n X Y | FF => nfa_for_bot n | Imp s t => nfa_for_imp (nfa_of_form n s) (nfa_of_form n t) | Ex s => nfa_for_ex (nfa_of_form n.+1 s) end.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)