diff --git a/tests/proofmode_monpred.ref b/tests/proofmode_monpred.ref
index 92732da479de702cb0cb1e47ab868ceb281efea2..8426e3b26ad338a12b75f2ac4db7d96e4a862575 100644
--- a/tests/proofmode_monpred.ref
+++ b/tests/proofmode_monpred.ref
@@ -35,3 +35,14 @@
   --------------------------------------∗
   ∀ i : I, 𝓟 ∗ 𝓠 ∗ Q i
   
+1 subgoal
+  
+  I : biIndex
+  PROP : sbi
+  FU0 : BiFUpd PROP * ()
+  P, Q : monpred.monPred I PROP
+  i : I
+  ============================
+  --------------------------------------∗
+  (Q -∗ emp) i
+  
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 3a2c65d6031ed1cfc0bb5ed21fbeb79ef060023b..a61e964708ea4714bc051e3057b97575ab4c743b 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -120,7 +120,12 @@ Section tests.
     iIntros "[$ #HP]". iFrame "HP".
   Qed.
 
+  Lemma test_iFrame_monPred_at_wand (P Q : monPred) i :
+    P i -∗ (Q -∗ P) i.
+  Proof. iIntros "$". Show. Abort.
+
   Lemma test_iNext_Bi P :
     @bi_entails monPredI (â–· P) (â–· P).
   Proof. iIntros "H". by iNext. Qed.
+
 End tests.