proposition: Lemma collP p q : reflect (coll p q) (collb p q).
proof: Proof. apply: (iffP idP). - move/dec_eq => H x. by move/eqP: (H x). - move => H. apply/dec_eq => x. apply/eqP. exact: 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)