fact: Definition dfa_to_cf : classifier_for (dfa_lang A) := {| cf_classifier := Classifier (delta_s A); cf_congruent := delta_s_right_congruent; cf_refines := delta_s_refines |}.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa minimization regexp)