fact: Definition dfa2_to_myhill := {| cf_classifier := Classifier Tab'; cf_congruent := image_rc; cf_refines := image_refines |}.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)