proposition: Lemma op_leq_weq_1 {h k X Y} {HX: laws h X} {HY: laws k Y} {f: X -> Y} {Hf: Proper (leq ==> leq) f}: Proper (weq ==> weq) f.
proof: Proof. intros x y. rewrite 2weq_spec. intro E; split; apply Hf; apply E. Qed.
imports: common level