proposition: Lemma classifier_to_dfa_correct : dfa_lang classifier_to_dfa =i L.
proof: Proof. move => w. rewrite -delta_lang classifier_to_dfa_delta inE. apply: imfun_of_refines. by rewrite crK. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa minimization regexp)