proposition: Lemma delta_iso_inv w x : delta (iso_inv x) w \in dfa_fin A = (delta x w \in dfa_fin B).
proof: Proof. Proof using L_AB. by rewrite -{2}[x](crK (Sf := B_conn)) -!delta_cat !delta_lang L_AB. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)