diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 4aa097847bdced00066e48a4355db957bc1d34eb..1ed83a72fee986a25e3bb839fa527b01660ebeff 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -233,9 +233,6 @@ Qed.
 Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
   x1 = x2 → (⌜ x2 = x3 ⌝ ∗ ⌜ x3 ≡ x4 ⌝ ∗ P) -∗ ⌜ x1 = x4 ⌝ ∗ P.
 Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
-
-Lemma test_iItros_pure : (⌜ ¬False ⌝ : uPred M)%I.
-Proof. by iIntros (?). Qed.
 End tests.
 
 Section more_tests.