diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index d2172c5d3ae4ebdbd92f8ad1ff297cca5be3ca61..9c002eaf9ca8ed761e317a85ac27b790442e4091 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -79,9 +79,9 @@ Proof. rewrite /AsValid=> ->. rewrite bi_embed_valid //. Qed.
 Tactic Notation "iStartProof" uconstr(PROP) :=
   lazymatch goal with
   | |- @envs_entails ?PROP' _ _ =>
-    let x := type_term (eq_refl : PROP = PROP') in idtac
+    let x := type_term (eq_refl : @eq Type PROP PROP') in idtac
   | |- let _ := _ in _ => fail
-  | |- ?φ => eapply (@as_valid_2 φ PROP);
+  | |- ?φ => eapply (λ P : PROP, @as_valid_2 φ _ P);
                [apply _ || fail "iStartProof: not a Bi entailment"
                |apply tac_adequate]
   end.
diff --git a/theories/tests/proofmode_iris.v b/theories/tests/proofmode_iris.v
index ec136a553766ebe890b304ab87e38872e93276aa..f22e3838ee11d88973c94d78cc60d124ee9878f4 100644
--- a/theories/tests/proofmode_iris.v
+++ b/theories/tests/proofmode_iris.v
@@ -36,6 +36,15 @@ Section base_logic_tests.
 
   Lemma test_iAssert_modality P : (|==> False) -∗ |==> P.
   Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
+
+  Lemma test_iStartProof_1 P : P -∗ P.
+  Proof. iStartProof. iStartProof. iIntros "$". Qed.
+  Lemma test_iStartProof_2 P : P -∗ P.
+  Proof. iStartProof (uPred _). iStartProof (uPredI _). iIntros "$". Qed.
+  Lemma test_iStartProof_3 P : P -∗ P.
+  Proof. iStartProof (uPredI _). iStartProof (uPredSI _). iIntros "$". Qed.
+  Lemma test_iStartProof_4 P : P -∗ P.
+  Proof. iStartProof (uPredSI _). iStartProof (uPred _). iIntros "$". Qed.
 End base_logic_tests.
 
 Section iris_tests.