proposition: Lemma proper_weq_leq_iff n m (P: X n m -> Prop): Proper (weq ==> impl) P -> Proper (weq ==> iff) P.
proof: Proof. intros HP ? ? E. split; now apply HP. Qed.
imports: common lattice monoid kleene normalisation rewriting