diff --git a/tests/monotone.ref b/tests/monotone.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/monotone.v b/tests/monotone.v
new file mode 100644
index 0000000000000000000000000000000000000000..b5e65ef77e83ff89139cb0bef0934dc72c872f3f
--- /dev/null
+++ b/tests/monotone.v
@@ -0,0 +1,14 @@
+Require Import iris.unstable.algebra.monotone.
+
+Section test_mra_over_ofe.
+  Context {A : ofe} {R : relation A}.
+  Implicit Types a b : A.
+  Implicit Types x y : mra R.
+
+  Context `{!Reflexive R} {Has : AntiSymm (≡) R}.
+  Lemma test a b : principal R a ≡ principal R b → a ≡ b.
+  Proof.
+    Fail by intros ?%(inj _).
+    by intros ?%(inj (R := equiv) _).
+  Qed.
+End test_mra_over_ofe.