proposition: Lemma w_weq: Proper (weq ==> weq) w.
proof: Proof. intros ? ? H. apply (H (expr_ops _ _ _) _ (fun _ => xH)). Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms