diff --git a/tests/proofmode.v b/tests/proofmode.v
index d86cebeac7ed571bdf6e8d98707ad349ab2a1dbd..67aca0959d6c7c62334c98af4d19a4c7ea4b369e 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -299,7 +299,7 @@ Lemma test_iIntros_let P :
   ∀ Q, let R := emp%I in P -∗ R -∗ Q -∗ P ∗ Q.
 Proof. iIntros (Q R) "$ _ $". Qed.
 
-Lemma test_foo P Q : <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
+Lemma test_iNext_iRewrite P Q : <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
 Proof.
   iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ".
 Qed.