diff --git a/_CoqProject b/_CoqProject
index f467b8c0a774a89f8cf345251087150e03302efe..e3a98170f1f67a6a5a086700759d8b9a519a33d5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -97,6 +97,7 @@ theories/tests/heap_lang.v
 theories/tests/one_shot.v
 theories/tests/proofmode.v
 theories/tests/proofmode_iris.v
+theories/tests/proofmode_monPred.v
 theories/tests/list_reverse.v
 theories/tests/tree_sum.v
 theories/tests/ipm_paper.v
diff --git a/theories/tests/proofmode_monPred.v b/theories/tests/proofmode_monPred.v
new file mode 100644
index 0000000000000000000000000000000000000000..e9f2053eaa6aaa9166ab7ff808c2e83b74d2856f
--- /dev/null
+++ b/theories/tests/proofmode_monPred.v
@@ -0,0 +1,30 @@
+From iris.proofmode Require Import tactics monpred.
+From iris.base_logic Require Import base_logic lib.invariants.
+
+Section tests.
+  Context {I : bi_index} {PROP : sbi}.
+  Local Notation monPred := (monPred I PROP).
+  Local Notation monPredI := (monPredI I PROP).
+  Local Notation monPredSI := (monPredSI I PROP).
+  Implicit Types P Q R : monPred.
+  Implicit Types i j : I.
+
+  Lemma test0 P : P -∗ P.
+  Proof. iIntros "$". Qed.
+
+  Lemma test_iStartProof_1 P : P -∗ P.
+  Proof. iStartProof. iStartProof. iIntros "$". Qed.
+  Lemma test_iStartProof_2 P : P -∗ P.
+  Proof. iStartProof monPred. iStartProof monPredI. iIntros "$". Qed.
+  Lemma test_iStartProof_3 P : P -∗ P.
+  Proof. iStartProof monPredI. iStartProof monPredSI. iIntros "$". Qed.
+  Lemma test_iStartProof_4 P : P -∗ P.
+  Proof. iStartProof monPredSI. iStartProof monPred. iIntros "$". Qed.
+  Lemma test_iStartProof_5 P : P -∗ P.
+  Proof. iStartProof PROP. iIntros (i) "$". Qed.
+  Lemma test_iStartProof_6 P : P ⊣⊢ P.
+  Proof. iStartProof PROP. iIntros (i). iSplit; iIntros "$". Qed.
+  Lemma test_iStartProof_7 P : ((P ≡ P)%I : monPredI).
+  Proof. iStartProof PROP. done. Qed.
+
+End tests.
\ No newline at end of file