fact: Fixpoint lang' (e: ugregex') (w: trace Atom) := match w with | tnil a => is_true (epsilon (set.mem a) e) | tcons a i w => lang' (deriv a i e) w end.
imports: kat lsyntax positives sups glang comparisons boolean