diff --git a/tests/proofmode_monpred.ref b/tests/proofmode_monpred.ref
index 459ec829a8026efcd2bc56fe91bd2f4d73e794f0..5b018493c4145a41a19a6427e308a55205e38378 100644
--- a/tests/proofmode_monpred.ref
+++ b/tests/proofmode_monpred.ref
@@ -62,3 +62,31 @@ In nested Ltac calls to "iFrame (constr)",
 "<iris.proofmode.ltac_tactics.iFrame_go>" and
 "<iris.proofmode.ltac_tactics.iFrameHyp>", last call failed.
 Tactic failure: iFrame: cannot frame (P i).
+1 subgoal
+  
+  I : biIndex
+  Σ : gFunctors
+  invG0 : invG Σ
+  N : namespace
+  P : iProp Σ
+  ============================
+  "H" : ⎡ inv N (<pers> P) ⎤
+  "H2" : ⎡ ▷ <pers> P ⎤
+  --------------------------------------â–¡
+  |={⊤ ∖ ↑N}=> ⎡ ▷ <pers> P ⎤ ∗ (|={⊤}=> ⎡ ▷ P ⎤)
+  
+1 subgoal
+  
+  I : biIndex
+  Σ : gFunctors
+  invG0 : invG Σ
+  N : namespace
+  P : iProp Σ
+  ============================
+  "H" : ⎡ inv N (<pers> P) ⎤
+  "H2" : ⎡ ▷ <pers> P ⎤
+  --------------------------------------â–¡
+  "Hclose" : ⎡ ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp ⎤
+  --------------------------------------∗
+  |={⊤ ∖ ↑N,⊤}=> ⎡ ▷ P ⎤
+