proposition: Lemma collapse_delta (x : A) w : delta (\pi x : collapse) w = \pi (delta x w).
proof: Proof. elim: w x => //= a w IHw x. rewrite -IHw. f_equal. apply/eqmodP. apply: collb_step. exact: epiK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)