fact: Record classifier_for L := { cf_classifier :> classifier; cf_congruent : right_congruent cf_classifier; cf_refines : refines L cf_classifier }.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa minimization regexp)