proposition: Lemma o'_weq n m: Proper (weq ==> weq) (@o' n m).
proof: Proof. intros ? ? H. apply (H (gregex_monoid_ops _ _ _) _ id). Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms