diff --git a/iris_unstable/algebra/monotone.v b/iris_unstable/algebra/monotone.v
index 9cda8b08a8c4151d65e1ae36edd5502b8804ba53..e670ecd0946201f39963d2a8b5676c6ea7bd8490 100644
--- a/iris_unstable/algebra/monotone.v
+++ b/iris_unstable/algebra/monotone.v
@@ -171,13 +171,21 @@ End cmra.
 Global Arguments mraR {_} _.
 Global Arguments mraUR {_} _.
 
+(**
+If [R] is a partial order, relative to a setoid [S] on the carrier [A],
+then [principal R] is proper and injective.
+
+The following theory generalizes over an arbitrary setoid [S] and necessary properties,
+but is overly general, so we encapsulate the instances in an opt-in module.
+*)
+Module mra_over_rel.
 Section mra_over_rel.
   Context {A : Type} {R : relation A}.
   Implicit Types a b : A.
   Implicit Types x y : mra R.
   Implicit Type (S : relation A).
 
-  Global Instance principal_rel_proper S
+  #[export] Instance principal_rel_proper S
          `{!Proper (S ==> S ==> iff) R} `{!Reflexive S} :
     Proper (S ==> (≡)) (principal R).
   Proof. intros a1 a2 Ha; split; rewrite ->!below_principal, !Ha; done. Qed.
@@ -191,10 +199,15 @@ Section mra_over_rel.
     R a a → R b b → (R a b → R b a → S a b) → S a b.
   Proof. intros ??? Has; apply Has; apply principal_inj_related; auto. Qed.
 
-  Global Instance principal_inj {S} `{!Reflexive R} `{!AntiSymm S R} :
+  #[export] Instance principal_inj {S} `{!Reflexive R} `{!AntiSymm S R} :
     Inj S (≡) (principal R).
   Proof. intros ???. apply principal_inj_general => //. apply: anti_symm. Qed.
 End mra_over_rel.
+End mra_over_rel.
+
+(* Specialize [mra_over_rel] to equality. Only [principal_inj] seems generally useful. *)
+Global Instance principal_inj `{R : relation A} `{!Reflexive R} `{!AntiSymm (=) R} :
+  Inj (=) (≡) (principal R) := mra_over_rel.principal_inj.
 
 (* Might be useful if the type of elements is an OFE. *)
 Section mra_over_ofe.
@@ -202,6 +215,8 @@ Section mra_over_ofe.
   Implicit Types a b : A.
   Implicit Types x y : mra R.
 
+  Import mra_over_rel.
+
   Global Instance principal_proper
          `{!∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} :
     Proper ((≡) ==> (≡)) (principal R) := ne_proper _.
diff --git a/iris_unstable/base_logic/algebra.v b/iris_unstable/base_logic/algebra.v
index c962e56e42a0002932f665b6f2d1823f37eeceab..8a8f270114106b6741d14da1481130017b7f1f51 100644
--- a/iris_unstable/base_logic/algebra.v
+++ b/iris_unstable/base_logic/algebra.v
@@ -28,7 +28,7 @@ Section monotone.
   Proof.
     uPred.unseal. do 2 split; intros Hp.
     - exact: principal_injN.
-    - apply: principal_rel_proper Hp.
+    - apply: mra_over_rel.principal_rel_proper Hp.
   Qed.
 End monotone.
 End upred.
diff --git a/tests/monotone.v b/tests/monotone.v
index a3004521b2a3017aa320708203463f8156df71d1..9ee07a5208c5bc921cacb8b3fb7c161d183235f3 100644
--- a/tests/monotone.v
+++ b/tests/monotone.v
@@ -1,10 +1,25 @@
 Require Import iris.unstable.algebra.monotone.
 
+Section test_mra_over_eq.
+  Context {A : Type} {R : relation A}.
+  Context `{!Reflexive R} {Has : AntiSymm (=) R}.
+
+  Implicit Types a b : A.
+  Implicit Types x y : mra R.
+
+  Lemma test1 a b : principal R a ≡ principal R b → a = b.
+  Proof.
+    by intros ?%(inj _).
+  Qed.
+
+End test_mra_over_eq.
+
 Section test_mra_over_ofe.
   Context {A : ofe} {R : relation A}.
   Implicit Types a b : A.
   Implicit Types x y : mra R.
 
+  Import mra_over_rel.
   Context `{!Reflexive R} {Has : AntiSymm (≡) R}.
   Lemma test a b : principal R a ≡ principal R b → a ≡ b.
   Proof.