proposition: Lemma deriv_eq a i e: deriv a i e ≡ sup id (pderiv (set.mem a) i e).
proof: Proof. induction e; simpl; fold_ugregex. case eqb_pos. 2: reflexivity. now rewrite sup_singleton. reflexivity. rewrite union_app, sup_app. now apply cup_weq. assert (H: deriv a i e1 ⋅ e2 ≡ sup id (map (tod e2) (pderiv (set.mem a) i e1))). rewrite sup_map. setoid_rewrite <-(dotsumx (X:=ugregex_monoid_ops _)). now apply dot_weq. case epsilon. rewrite union_app, sup_app. setoid_rewrite dot1x. now apply cup_weq. setoid_rewrite dot0x. now rewrite cupxb. rewrite sup_map. setoid_rewrite <-(dotsumx (X:=ugregex_monoid_ops _)). now apply dot_weq. Qed.
imports: lset kat positives sums glang boolean comparisons powerfix ugregex