proposition: Lemma deriv_vars a i (e: ugregex): \sup_(x\in pderiv a i e) vars x ≦ vars e.
proof: Proof. induction e; simpl pderiv; simpl vars. case eqb_pos; apply leq_bx. apply leq_bx. rewrite 2union_app, sup_app. now apply cup_leq. setoid_rewrite union_app at 2. assert (H: \sup_(x\in map (tod e2) (pderiv a i e1)) vars x ≦ vars e1 ++ vars e2). rewrite sup_map. simpl vars. setoid_rewrite union_app. rewrite supcup. apply cup_leq. assumption. now apply leq_supx. case epsilon. rewrite union_app, sup_app, H. hlattice. assumption. rewrite sup_map. simpl vars. setoid_rewrite union_app. rewrite supcup. apply leq_cupx. assumption. now apply leq_supx. Qed.
imports: lset kat positives sums glang boolean comparisons powerfix ugregex