fact: Definition coll (A : dfa) x y := forall w, (delta x w \in dfa_fin A) = (delta y w \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)