proposition: Lemma deriv'_eq a i l: deriv a i (sup id l) ≡ sup id (pderiv' (set.mem a) i l).
proof: Proof. induction l. reflexivity. simpl (sup _ _). rewrite union_app, sup_app. apply cup_weq. apply deriv_eq. assumption. Qed.
imports: lset kat positives sums glang boolean comparisons powerfix ugregex