fact: Definition mg_to_classifier L (N : mgClassifier L) := {| cf_congruent := @mg_right_congruent L N; cf_refines := @mg_refines L N |}.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa minimization regexp)