proposition: Lemma collapse_size A : #|collapse A| <= #|A|.
proof: Proof. rewrite card_sub. exact: max_card. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)