diff --git a/tests/proofmode.v b/tests/proofmode.v
index 27b0a34e1f1de36da34a5ae7c63d143e420d6cc8..b0d52b54cdda219b960312d704bb64e2e07e74f4 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -239,6 +239,14 @@ Proof.
   iFrame.
 Qed.
 
+Lemma test_iExists_unused : (∃ P : PROP, ∃ x : nat, P)%I.
+Proof.
+  iExists _.
+  iExists 10.
+  iAssert emp%I as "H"; first done.
+  iExact "H".
+Qed.
+
 (* Check coercions *)
 Lemma test_iExist_coercion (P : Z → PROP) : (∀ x, P x) -∗ ∃ x, P x.
 Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.