fact: Record nfa : Type := { nfa_state :> finType; nfa_s : { set nfa_state }; nfa_fin : { set nfa_state }; nfa_trans : nfa_state -> char -> nfa_state -> bool }.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)