diff --git a/lib/ModuRes/Predom.v b/lib/ModuRes/Predom.v
index 34a2fc44f2f653ba7eaea6005653641557893f98..1be4159b1e9f7542de84c5d7b8130da3aa54cd70 100644
--- a/lib/ModuRes/Predom.v
+++ b/lib/ModuRes/Predom.v
@@ -8,8 +8,15 @@ Class preoType T {eqT : Setoid T} :=
   {pord   :  relation T;
    preoPO :> PreOrder pord;
    preoC  : Proper (equiv ==> equiv ==> impl) pord}.
-   
-Instance preoType_compat T `{pT : preoType T} : Proper (equiv ==> equiv ==> impl) pord := preoC.
+
+(** Rewriting under pord. *)
+Instance preoType_compat T `{pT : preoType T} : Proper (equiv ==> equiv ==> iff) pord.
+Proof.
+  split; first by exact: preoC.
+  symmetry in H, H0.
+  exact: preoC.
+Qed.
+
 Arguments pord {_ _ _} !_ !_.
 Notation "'mkPOType' R" := (Build_preoType _ _ R _) (at level 10).
 Notation "s ⊑ t" := (pord s t) (at level 70, no associativity) : predom_scope.