diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 5ea81c851ffa28981b586b35f2b342c66004d11c..b32d5780a5c81cddebd1eeeef7b8bedf087d4706 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -146,3 +146,10 @@ Proof. eauto with iFrame. Qed.
 Lemma demo_17 (M : ucmraT) (P Q R : uPred M) `{!PersistentP R} :
   P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False.
 Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed.
+
+Lemma test_iNext_evar (M : ucmraT) (P : uPred M) :
+  P -∗ True.
+Proof.
+  iIntros "HP". iAssert (▷ _ -∗ ▷ P)%I as "?"; last done.
+  iIntros "?". iNext. iAssumption.
+Qed.