diff --git a/tests/proofmode.v b/tests/proofmode.v
index 7ebd11da3560c6f616c69d120a05cdbda8ed2b21..9dec1daa99436b5b81803357d6dce5187183eff9 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1420,6 +1420,11 @@ Proof.
   iIntros (?) "HP HQ". iModIntro. Show. by iFrame.
 Qed.
 
+Lemma test_iExfalso_start_proof P : 0 = 1 → ⊢ P.
+Proof.
+  intros. iExFalso. done.
+Qed.
+
 Check "test_iRevert_pure".
 Lemma test_iRevert_pure (φ : Prop) P :
   φ → (<affine> ⌜ φ ⌝ -∗ P) -∗ P.