diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index a5eb0623da91cb9c6b90be486158689db9b76bc6..f8c169ca0efcd66de0f7c113530c24db7bde75c5 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -154,10 +154,16 @@ Proof.
   iIntros "?". iNext. iAssumption.
 Qed.
 
-Lemma test_iNext_sep (M : ucmraT) (P Q : uPred M)
+Lemma test_iNext_sep1 (M : ucmraT) (P Q : uPred M)
     (R1 := (P âˆ— Q)%I) (R2 := (â–· P âˆ— â–· Q)%I) :
   (â–· P âˆ— â–· Q) âˆ— R1 âˆ— R2 -âˆ— â–· (P âˆ— Q) âˆ— â–· R1 âˆ— R2.
 Proof.
   iIntros "H". iNext.
   rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done.
 Qed.
+
+Lemma test_iNext_sep2 (M : ucmraT) (P Q : uPred M) :
+  â–· P âˆ— â–· Q -âˆ— â–· (P âˆ— Q).
+Proof.
+  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
+Qed.