proposition: Lemma collapse_connected A : connected A -> connected (collapse A).
proof: Proof. move => H x. case: (H (repr x)) => w /eqP Hw. exists w. by rewrite /delta_s collapse_delta -/(delta_s A w) Hw 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)