proposition: Lemma collapse_collapsed (A : dfa) : collapsed (collapse A).
proof: Proof. split => [H|->]; last by apply/collP; exact: collb_refl. rewrite -[x]reprK -[y]reprK. apply/eqmodP/collP => w. by rewrite -!collapse_fin -!collapse_delta !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)