proposition: Lemma collapse_fin (x : A) : (\pi x \in dfa_fin collapse) = (x \in dfa_fin A).
proof: Proof. rewrite /collapse /= inE. by move/collP: (epiK collb_equiv x) => /(_ [::]). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)