proposition: Lemma minimal_iso A B : dfa_lang A =i dfa_lang B -> minimal A -> minimal B -> dfa_iso A B.
proof: Proof. move => L_AB /minimalP [? ?] /minimalP [? ?]. exact: coll_iso. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)