diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 97d711b50deb55750f2b5607113a630ef79f3afb..aa433d1c85eb29566bb916f268d57487f0ed73de 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -303,6 +303,14 @@ Lemma test_iNext_plus_3 P Q n m k :
   ▷^m ▷^(2 + S n + k) P -∗ ▷^m ▷ ▷^(2 + S n) Q -∗ ▷^k ▷ ▷^(S (S n + S m)) (P ∗ Q).
 Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Qed.
 
+Lemma test_iNext_unfold P Q n m (R := (â–·^n P)%I) :
+  R ⊢ ▷^m True.
+Proof.
+  iIntros "HR". iNext.
+  match goal with |-  context [ R ] => idtac | |- _ => fail end.
+  done.
+Qed.
+
 Lemma test_iEval x y : ⌜ (y + x)%nat = 1 ⌝ -∗ ⌜ S (x + y) = 2%nat ⌝ : uPred M.
 Proof.
   iIntros (H).