test via printing that the goal looks like it should

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

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. *)