proposition: Lemma dfa_prune_size : #|dfa_prune| <= #|A|.
proof: Proof. by rewrite card_sig subset_leq_card // subset_predT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)