diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 4dcf318a55376e2d6e11d2e5883a26b64b5465f9..558ea48baf19235818a5ab9f5a8f856e89caef0b 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -31,6 +31,17 @@
   --------------------------------------â–¡
   <affine> (P ∗ Q)
   
+1 subgoal
+  
+  PROP : sbi
+  H : BiAffine PROP
+  P, Q : PROP
+  ============================
+  _ : â–¡ P
+  _ : Q
+  --------------------------------------∗
+  â–¡ P
+  
 1 subgoal
   
   PROP : sbi
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 3905f8bb75bd8dc857930ed5bc7d9c27b080d08d..2c340bc11178f525af7071626c0c2b02d3b340e5 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -482,9 +482,9 @@ Qed.
 
 Lemma test_and_sep_affine_bi `{BiAffine PROP} P Q : □ P ∧ Q ⊢ □ P ∗ Q.
 Proof.
-  iIntros "[??]". iSplit; last done.
-  lazymatch goal with |- coq_tactics.envs_entails _ (â–¡ P) => done end.
+  iIntros "[??]". iSplit; last done. Show. done.
 Qed.
+
 End tests.
 
 (** Test specifically if certain things print correctly. *)