proposition: Lemma coll_iso : dfa_iso A B.
proof: Proof. Proof using A_coll B_coll A_conn B_conn L_AB. exists iso. split. - exact: Bijective can_iso_inv can_iso. - move => x a. apply/B_coll => w. rewrite -[_ (iso x) a]/(delta (iso x) [::a]). by rewrite -delta_cat -!delta_iso_inv !can_iso_inv. - move => x. by rewrite -[iso x]/(delta _ [::]) delta_iso. - apply/B_coll => w. by rewrite delta_iso !delta_lang. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)