fact: Definition nfa_for_incl n X Y := {| nfa_state := unit; nfa_s := setT; nfa_fin := setT; nfa_trans := fun p (v : vec n) q => nth false v X ==> nth false v Y |}.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)