diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 5806a9ee19da59341b3d2adfa099ec7528828052..a69d2e12221f3638875649ae77854d30105393a9 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -13,7 +13,7 @@ Section bool.
          | [ #(LitInt (0|1))] => True
          | _ => False
          end%I |}.
-  Next Obligation. intros ? [|[[| |[|[]|]]|] []]; iStartProof; auto. Qed.
+  Next Obligation. intros ? [|[[| |[|[]|]]|] []]; auto with I. Qed.
   Next Obligation. intros ? [|[[| |[|[]|]]|] []]; apply _. Qed.
 
   Global Instance bool_send : Send bool.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index af9b3615c3ea7385cc23c29def929b25f180d86e..a717024669b508df14d3440ffd9bc277021e5c0f 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -12,7 +12,7 @@ Section int.
          | [ #(LitInt z)] => True
          | _ => False
          end%I |}.
-  Next Obligation. intros ? [|[[]|] []]; iStartProof; auto. Qed.
+  Next Obligation. intros ? [|[[]|] []]; auto with I. Qed.
   Next Obligation. intros ? [|[[]|] []]; apply _. Qed.
 
   Global Instance int_send : Send int.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index dc0d11b991dcdd6f9289aae7033da0e3a439a3d3..c1eb039300efc46abfd6df82cace6974198c4b85 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -56,8 +56,7 @@ Section type_context.
     destruct (eval_path p1); try (intros ?; by iApply wp_value); [].
     destruct v0; try discriminate; [].
     destruct l; try discriminate; [].
-    intros [=<-]. iStartProof. wp_bind p1.
-    iApply (wp_wand with "[]").
+    intros [=<-]. wp_bind p1. iApply (wp_wand with "[]").
     { iApply IHp1. done. }
     iIntros (v) "%". subst v. wp_op. done.
   Qed.