diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index 8532b48176dfa8d80a06d62143e5be4e3c729b93..4281ec6ef199f51573c03d0c1d03be3c69ca5219 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -64,4 +64,9 @@ Section tests.
   Proof.
     iStartProof. iIntros (n) "$".
   Qed.
+
+  Lemma test_embed_wand (P Q : PROP) : (⎡P⎤ -∗ ⎡Q⎤) -∗ ⎡P -∗ Q⎤ : monPred.
+  Proof.
+    iIntros "H HP". by iApply "H".
+  Qed.
 End tests.