diff --git a/tests/monpred.ref b/tests/monpred.ref
new file mode 100644
index 0000000000000000000000000000000000000000..4cbbc11183db0ed024ec6fc7fc3c8711ccc0b83b
--- /dev/null
+++ b/tests/monpred.ref
@@ -0,0 +1,21 @@
+"monPred_unseal_test_1"
+     : string
+1 goal
+  
+  I : biIndex
+  M : ucmra
+  P, Q : uPredI M
+  R : monPred
+  i : I
+  ============================
+  (P ∗ Q) ∗ R i ⊣⊢ False
+"monPred_unseal_test_2"
+     : string
+1 goal
+  
+  I : biIndex
+  M : ucmra
+  P, Q : uPredI M
+  R : monPred
+  ============================
+  ⎡ upred.uPred_sep_def P Q ⎤ ∗ R ⊣⊢ False
diff --git a/tests/monpred.v b/tests/monpred.v
new file mode 100644
index 0000000000000000000000000000000000000000..26e467e11ba8304dc6458c963506ec358bb32766
--- /dev/null
+++ b/tests/monpred.v
@@ -0,0 +1,27 @@
+From stdpp Require Import strings.
+From iris.base_logic Require Import bi.
+From iris.bi Require Import embedding monpred.
+
+Section tests_unseal.
+  Context {I : biIndex} (M : ucmra).
+
+  Local Notation monPred := (monPred I (uPredI M)).
+
+  Check "monPred_unseal_test_1".
+  Lemma monPred_unseal_test_1 P Q (R : monPred) :
+    ⎡ P ∗ Q ⎤ ∗ R ⊣⊢ False.
+  Proof.
+    intros. split=> i. monPred.unseal.
+    (** Make sure [∗] on uPred is not unfolded *)
+    Show.
+  Abort.
+
+  Check "monPred_unseal_test_2".
+  Lemma monPred_unseal_test_2 P Q (R : monPred) :
+    ⎡ P ∗ Q ⎤ ∗ R ⊣⊢ False.
+  Restart.
+    uPred.unseal.
+    (** Make sure [∗] on monPred is not unfolded *)
+    Show.
+  Abort.
+End tests_unseal.