diff --git a/tests/proofmode_monpred.ref b/tests/proofmode_monpred.ref
index 5b018493c4145a41a19a6427e308a55205e38378..72d54d672894514f9517e13d8894a112866e7edd 100644
--- a/tests/proofmode_monpred.ref
+++ b/tests/proofmode_monpred.ref
@@ -68,12 +68,12 @@ Tactic failure: iFrame: cannot frame (P i).
   Σ : gFunctors
   invG0 : invG Σ
   N : namespace
-  P : iProp Σ
+  𝓟 : iProp Σ
   ============================
-  "H" : ⎡ inv N (<pers> P) ⎤
-  "H2" : ⎡ ▷ <pers> P ⎤
+  "H" : ⎡ inv N (<pers> 𝓟) ⎤
+  "H2" : ⎡ ▷ <pers> 𝓟 ⎤
   --------------------------------------□
-  |={⊤ ∖ ↑N}=> ⎡ ▷ <pers> P ⎤ ∗ (|={⊤}=> ⎡ ▷ P ⎤)
+  |={⊤ ∖ ↑N}=> ⎡ ▷ <pers> 𝓟 ⎤ ∗ (|={⊤}=> ⎡ ▷ 𝓟 ⎤)
   
 1 subgoal
   
@@ -81,12 +81,12 @@ Tactic failure: iFrame: cannot frame (P i).
   Σ : gFunctors
   invG0 : invG Σ
   N : namespace
-  P : iProp Σ
+  𝓟 : iProp Σ
   ============================
-  "H" : ⎡ inv N (<pers> P) ⎤
-  "H2" : ⎡ ▷ <pers> P ⎤
+  "H" : ⎡ inv N (<pers> 𝓟) ⎤
+  "H2" : ⎡ ▷ <pers> 𝓟 ⎤
   --------------------------------------□
-  "Hclose" : ⎡ ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp ⎤
+  "Hclose" : ⎡ ▷ <pers> 𝓟 ={⊤ ∖ ↑N,⊤}=∗ emp ⎤
   --------------------------------------∗
-  |={⊤ ∖ ↑N,⊤}=> ⎡ ▷ P ⎤
+  |={⊤ ∖ ↑N,⊤}=> ⎡ ▷ 𝓟 ⎤
   
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 41c98a1409bd760d003d0d340690d675de8dbf80..013a1e199f6b613301384c2716257d877ced6385 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -174,18 +174,19 @@ Section tests_iprop.
   Context {I : biIndex} `{!invG Σ}.
 
   Local Notation monPred := (monPred I (iPropI Σ)).
-  Implicit Types P : iProp Σ.
+  Implicit Types P Q R : monPred.
+  Implicit Types 𝓟 𝓠 𝓡 : iProp Σ.
 
-  Lemma test_iInv_0 N P:
-    embed (B:=monPred) (inv N (<pers> P)) ={⊤}=∗  ⎡▷ P⎤.
+  Lemma test_iInv_0 N 𝓟 :
+    embed (B:=monPred) (inv N (<pers> 𝓟)) ={⊤}=∗ ⎡▷ 𝓟⎤.
   Proof.
     iIntros "#H".
     iInv N as "#H2". Show.
     iModIntro. iSplit=>//. iModIntro. iModIntro; auto.
   Qed.
 
-  Lemma test_iInv_0_with_close N P:
-    embed (B:=monPred) (inv N (<pers> P)) ={⊤}=∗ ⎡▷ P⎤.
+  Lemma test_iInv_0_with_close N 𝓟 :
+    embed (B:=monPred) (inv N (<pers> 𝓟)) ={⊤}=∗ ⎡▷ 𝓟⎤.
   Proof.
     iIntros "#H".
     iInv N as "#H2" "Hclose". Show.