fact: Definition dfa_iso (A1 A2 : dfa) := exists i: A1 -> A2, [/\ bijective i, forall x a, i (dfa_trans x a) = dfa_trans (i x) a, forall x, i (x) \in dfa_fin A2 = (x \in dfa_fin A1) & i (dfa_s A1) = dfa_s A2 ].
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)