fact: Fixpoint lang (e: ugregex): uglang := match e with | u_var a => tsingle a | u_prd p => tinj (fun i => eval (set.mem i) p) | u_pls e f => lang e + lang f | u_dot e f => lang e ⋅ lang f | u_itr e => (lang e)^+ end.
imports: kat lsyntax positives sups glang comparisons boolean