fact: Definition KFinite (E : gset A) : Prop := exists l, (forall x:A, E x <-> INA l x).
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)