proposition: Lemma collb_step a x y : collb x y -> collb (dfa_trans x a) (dfa_trans y a).
proof: Proof. move => /collP H. apply/collP => w. by rewrite !delta_cons H. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)