proposition: Lemma cf_lang_eq_proof L1 L2 (M1 : classifier_for L1) : L1 =i L2 -> refines L2 M1.
proof: Proof. move => H0 u v /cf_refines. by rewrite -!H0. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa minimization regexp)