also add my original testcase, just to be sure

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.