fact: Record enfa : Type := { enfa_state :> finType; enfa_s : {set enfa_state}; enfa_f : {set enfa_state}; enfa_trans : option char -> enfa_state -> enfa_state -> bool }.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)