proposition: Lemma dfa_prune_correct : dfa_lang dfa_prune =i dfa_lang A.
proof: Proof. rewrite /dfa_lang /= -[dfa_s A]/(val reachable_s) => w. rewrite !inE. elim: w (reachable_s) => [|a w IHw] [x Hx] //=. + by rewrite /dfa_accept inE. + by rewrite accE IHw. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)