diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index a44213e29f0fe5629185493be7347522ffaf7478..4a389531742aba7b0d37059883f0e8aa71f1a1fc 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -181,6 +181,19 @@ Proof.
   iLöb as "IH". iDestruct "IH" as (n) "IH".
   by iExists (S n).
 Qed.
+
+Lemma test_iIntros_start_proof :
+  (True : uPred M)%I.
+Proof.
+  (* Make sure iIntros actually makes progress and enters the proofmode. *)
+  progress iIntros. done.
+Qed.
+
+Lemma test_True_intros : (True : uPred M) -∗ True.
+Proof.
+  iIntros "?". done.
+Qed.
+
 End tests.
 
 Section more_tests.