fact: Definition eqb_kat (e f: ugregex) := let atoms := map (@set.mem _) (seq _) in let vars := vars (e+f) in loop vars atoms 1000 rel_empty [([e],[f])%list].
imports: lset kat positives sums glang boolean comparisons powerfix ugregex