diff --git a/iris/resources.v b/iris/resources.v
index 632a15d302923a053d365928a507f30832d69c73..725d36f323f85154b5a71193c260cc918aed284c 100644
--- a/iris/resources.v
+++ b/iris/resources.v
@@ -41,8 +41,8 @@ Global Instance pst_ne' n : Proper (dist (S n) ==> (≡)) (@pst Σ A).
 Proof.
   intros σ σ' [???]; apply (timeless _), dist_le with (S n); auto with lia.
 Qed.
-Global Instance pst_proper : Proper ((≡) ==> (≡)) (@pst Σ A).
-Proof. by destruct 1. Qed.
+Global Instance pst_proper : Proper ((≡) ==> (=)) (@pst Σ A).
+Proof. by destruct 1; unfold_leibniz. Qed.
 Global Instance gst_ne n : Proper (dist n ==> dist n) (@gst Σ A).
 Proof. by destruct 1. Qed.
 Global Instance gst_proper : Proper ((≡) ==> (≡)) (@gst Σ A).
diff --git a/modures/auth.v b/modures/auth.v
index eedff69790974874941ca74c074815e3c8e7dbcc..c821b5de3403683480c144800dda7befa9b2e24f 100644
--- a/modures/auth.v
+++ b/modures/auth.v
@@ -45,6 +45,8 @@ Canonical Structure authC := CofeT auth_cofe_mixin.
 Instance Auth_timeless (x : excl A) (y : A) :
   Timeless x → Timeless y → Timeless (Auth x y).
 Proof. by intros ?? [??] [??]; split; simpl in *; apply (timeless _). Qed.
+Global Instance auth_leibniz : LeibnizEquiv A → LeibnizEquiv (auth A).
+Proof. by intros ? [??] [??] [??]; f_equal'; apply leibniz_equiv. Qed.
 End cofe.
 
 Arguments authC : clear implicits.
diff --git a/modures/cofe.v b/modures/cofe.v
index 1b8913b96f73a28e2e3877142268fa9e8aae03b7..f8d32d84a5a409263aacf6a1d89b65f5a9c738db 100644
--- a/modures/cofe.v
+++ b/modures/cofe.v
@@ -300,6 +300,9 @@ End discrete_cofe.
 Arguments discreteC _ {_ _}.
 
 Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _.
+Instance leibnizC_leibniz : LeibnizEquiv (leibnizC A).
+Proof. by intros A x y. Qed.
+
 Canonical Structure natC := leibnizC nat.
 Canonical Structure boolC := leibnizC bool.
 
diff --git a/modures/excl.v b/modures/excl.v
index 6382906841af3c652d47c7920414d1888e6e7840..fcac96f26af036c392f53fb6073006475f21faed 100644
--- a/modures/excl.v
+++ b/modures/excl.v
@@ -75,6 +75,8 @@ Proof. by inversion_clear 1; constructor. Qed.
 Global Instance excl_timeless :
   (∀ x : A, Timeless x) → ∀ x : excl A, Timeless x.
 Proof. intros ? []; apply _. Qed.
+Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A).
+Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
 
 (* CMRA *)
 Instance excl_valid : Valid (excl A) := λ x,