diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 100a162b6be4e8a282c90beb434c3e82b38346cb..6e2f09efef0b374c4a64b174a669897f2fc4d632 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -28,6 +28,18 @@
   --------------------------------------∗
   |={⊤ ∖ ↑N,⊤}=> ▷ P
   
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  γ : gname
+  p : Qp
+  N : namespace
+  P : iProp Σ
+  ============================
+  cinv N γ (<pers> P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P
 1 subgoal
   
   Σ : gFunctors
@@ -86,6 +98,20 @@
   |={⊤}=> (▷ <pers> P ∗ na_own t (E2 ∖ ↑N))
           ∗ (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
   
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  t : na_inv_pool_name
+  N : namespace
+  E1, E2 : coPset
+  P : iProp Σ
+  ============================
+  ↑N ⊆ E2
+  → na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
+    ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index e3e5102007459276eb9b88844bb4c6180599eff6..a01fafc469a8ce0a34a93f749c4b6b5366c451fa 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -101,6 +101,7 @@ Section iris_tests.
   Lemma test_iInv_2 γ p N P:
     cinv N γ (<pers> P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P.
   Proof.
+    Show.
     iIntros "(#?&?)".
     iInv N as "(#HP&Hown)". Show.
     iModIntro. iSplit; auto with iFrame.
@@ -139,6 +140,7 @@ Section iris_tests.
     na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
          ⊢ |={⊤}=> na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
+    Show.
     iIntros (?) "(#?&Hown1&Hown2)".
     iInv N as "(#HP&Hown2)" "Hclose". Show.
     iMod ("Hclose" with "[HP Hown2]").