fact: Definition dfa_prune := {| dfa_s := reachable_s; dfa_fin := [set x | val x \in dfa_fin A]; dfa_trans := reachable_trans |}.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)