fact: Definition nerode (X : eqType) (L : dlang char) (E : word -> X) := forall u v, E u = E v <-> forall w, (u++w \in L) = (v++w \in L).
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa minimization regexp)