diff --git a/tests/proofmode.v b/tests/proofmode.v
index 56aa97a8dc9efb0e3d2423f2d5afb5bcf187b14f..d84511d9d1fe9f618b54692199563f261eee3af9 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -778,9 +778,6 @@ Check "test_iSimpl_in4".
 Lemma test_iSimpl_in4 x y : ⌜ (3 + x)%nat = y ⌝ -∗ ⌜ S (S (S x)) = y ⌝ : PROP.
 Proof. iIntros "H". Fail iSimpl in "%". by iSimpl in "H". Qed.
 
-Lemma test_iIntros_pure_neg : ⊢@{PROP} ⌜ ¬False ⌝.
-Proof. by iIntros (?). Qed.
-
 Lemma test_iPureIntro_absorbing (φ : Prop) :
   φ → ⊢@{PROP} <absorb> ⌜φ⌝.
 Proof. intros ?. iPureIntro. done. Qed.