proposition: Lemma collapse_correct A : dfa_lang (collapse A) =i dfa_lang A.
proof: Proof. move => w. rewrite !inE /dfa_accept {1}/dfa_s /= inE collapse_delta. by rewrite -!collapse_fin reprK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)