fact: Definition collb p q : bool := allseq_dec (@coll_fun_RC p q) [pred p | (p.1 \in dfa_fin A) == (p.2 \in dfa_fin A)].
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)