proposition: Lemma classifier_to_dfa_delta : delta_s classifier_to_dfa =1 imfun_of.
proof: Proof. apply: last_ind => [|w a IHw] //=. rewrite /delta_s -cats1 delta_cat -!/(delta_s _ _) IHw. apply: imfun_of_congruent. by rewrite crK. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa minimization regexp)