diff --git a/tests/proofmode.v b/tests/proofmode.v
index d67a8b9d11264a7f481add5aad2c7df33a31fd6e..fc2de8e85c2d69e46ad958f8f421809be530128a 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1115,7 +1115,7 @@ Lemma test_iApply_prettification3 (Ψ Φ : nat → PROP) :
   Ψ 11 -∗ Φ 10.
 Proof.
   iIntros (HP) "H".
-  iApply HP.
+  iApply HP. (* should be [Ψ (1 + 10)], without a beta redex *)
   Show.
   iApply "H".
 Qed.