proposition: Lemma deriv'_vars a i l: \sup_(x\in pderiv' a i l) vars x ≦ sup vars l.
proof: Proof. induction l. reflexivity. setoid_rewrite union_app. rewrite sup_app. apply cup_leq. apply deriv_vars. assumption. Qed.
imports: lset kat positives sums glang boolean comparisons powerfix ugregex