diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index a79341f8a44eef7c657dcae213167430a5d1d6fc..5bd5a79f3c04b92233013ad522d9a269fa9b00a1 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -115,7 +115,7 @@ Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
   P -∗ Q → R -∗ emp.
 Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.
 
-Let test_fresh P Q:
+Lemma test_fresh P Q:
   (P ∗ Q) -∗ (P ∗ Q).
 Proof.
   iIntros "H".