proposition: Lemma dfa_prune_connected : connected dfa_prune.
proof: Proof. move => q. case/dec_eq: (svalP q) => /= x Hx. exists x. elim/last_ind : x q Hx => //= x a IHx q. rewrite -!cats1 /delta_s !delta_cat -!/(delta_s _ x) => H. have X : reachable (delta_s A x). apply/dec_eq; exists x. exact: eqxx. by rewrite (eqP (IHx (Sub (delta_s A x) 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)