fact: Definition nfa_char (a:char) := {| nfa_s := [set false]; nfa_fin := [set true]; nfa_trans p b q := if (p,q) is (false,true) then (b == a) else false |}.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)