proposition: Lemma epsilon'_eq a l: epsilon a (sup id l) ≡ epsilon' a l.
proof: Proof. induction l. reflexivity. simpl. rewrite <- IHl. unfold id. rewrite <-2Bool.orb_lazy_alt. apply Bool.orb_comm. Qed.
imports: lset kat positives sums glang boolean comparisons powerfix ugregex