diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index b0028a7dcb9c7f8c5adc828487bab27056d9ab4a..020f883e2ca17db120560445d04b36bb185c964a 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -8,15 +8,21 @@ Section typing.
   Context `{typeG Σ}.
 
   (** Jumping to and defining a continuation. *)
-  Lemma type_jump args E L C T k T' :
+  Lemma type_jump args argsv E L C T k T' :
+    (* We use this rather complicated way to state that
+         args = of_val <$> argsv, only because then solve_typing
+         is able to prove it easily. *)
+    Forall2 (λ a av, to_val a = Some av ∨ a = of_val av) args argsv →
     (k ◁cont(L, T'))%CC ∈ C →
-    tctx_incl E L T (T' (list_to_vec args)) →
-    typed_body E L C T (k (of_val <$> args)).
+    tctx_incl E L T (T' (list_to_vec argsv)) →
+    typed_body E L C T (k args).
   Proof.
-    iIntros (HC Hincl tid qE) "#LFT Htl HE HL HC HT".
+    iIntros (Hargs HC Hincl tid qE) "#LFT Hna HE HL HC HT".
     iMod (Hincl with "LFT HE HL HT") as "(HE & HL & HT)".
     iSpecialize ("HC" with "HE []"); first done.
-    rewrite -{3}(vec_to_list_of_list args). iApply ("HC" with "Htl HL HT").
+    assert (args = of_val <$> argsv) as ->.
+    { clear -Hargs. induction Hargs as [|a av ?? [<-%of_to_val| ->] _ ->]=>//=. }
+    rewrite -{3}(vec_to_list_of_list argsv). iApply ("HC" with "Hna HL HT").
   Qed.
 
   Lemma type_cont argsb L1 (T' : vec val (length argsb) → _) E L2 C T econt e2 kb :
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 1eabd4e3b07504b63bc5d67d016c50a7ce5096ee..91b7f70955d349bc6dbc4b8ac1aa594bf713b95e 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -22,6 +22,6 @@ Section get_x.
     iApply type_deref; [solve_typing..|]. iIntros (p'); simpl_subst.
     iApply (type_letalloc_1 (&shr{α}int)); [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_delete; [solve_typing..|].
-    iApply (type_jump [_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 End get_x.
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index b7da2ea5dfcc898922752ee4a5054107f1c9ba0f..76c97b277491a62475411ea0a84f457410965312 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -25,6 +25,6 @@ Section init_prod.
     iApply type_assign; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
-    iApply (type_jump [_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 End init_prod.
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 4c25cf38829e581859f9c41f9ea1d5b4c71f4da9..c498e9a97ff6ec2be206b08989df14043cdb52a3 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -41,6 +41,6 @@ Section lazy_lft.
     iApply (type_delete (Π[&shr{_}_;&shr{_}_])%T); [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
-    iApply (type_jump [_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 End lazy_lft.
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index 9d7a129778b8b222fe8e209806dc7c0f86fe3f6d..f3a30336d872d678ac795f7eac5752dcc2bb4165 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -32,6 +32,6 @@ Section rebor.
     iApply type_delete; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
-    iApply (type_jump [_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 End rebor.
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index b9b5734349158ee2b98410293564479866e26e48..85fb12ea03f23d528c2ffa38b3e0a55eb2a3d230 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -20,6 +20,6 @@ Section unbox.
     iApply type_deref_uniq_own; [solve_typing..|]. iIntros (bx); simpl_subst.
     iApply type_letalloc_1; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_delete; [solve_typing..|].
-    iApply (type_jump [_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 End unbox.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index dce104cb3562bc7400b1acbc266245e7bedc0375..1f27369931496d337d6ab94b18789cae3ae487b8 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -356,6 +356,26 @@ Arguments lctx_lft_eq {_ _ _} _%EL _%LL _ _.
 Arguments lctx_lft_alive {_ _ _} _%EL _%LL _.
 Arguments elctx_sat {_ _ _} _%EL _%LL _%EL.
 
+Lemma elctx_sat_cons_weaken `{invG Σ, lftG Σ} e0 E E' L :
+  elctx_sat E L E' → elctx_sat (e0 :: E) L E'.
+Proof.
+  iIntros (HE' ????). rewrite /elctx_interp. setoid_rewrite big_sepL_cons.
+  iIntros "[? HE] HL". iMod (HE' with "HE HL") as (?) "[H Hclose]". done.
+  auto 10 with iFrame.
+Qed.
+
+Lemma elctx_sat_app_weaken_l `{invG Σ, lftG Σ} E0 E E' L :
+  elctx_sat E L E' → elctx_sat (E0 ++ E) L E'.
+Proof. induction E0=>//= ?. auto using elctx_sat_cons_weaken. Qed.
+
+Lemma elctx_sat_app_weaken_r `{invG Σ, lftG Σ} E0 E E' L :
+  elctx_sat E L E' → elctx_sat (E ++ E0) L E'.
+Proof.
+  intros ?????. rewrite /elctx_sat /elctx_interp.
+  setoid_rewrite (big_opL_permutation _ (E++E0)); try apply Permutation_app_comm.
+  by apply elctx_sat_app_weaken_l.
+Qed.
+
 Section elctx_incl.
   (* External lifetime context inclusion, in a persistent context.
      (Used for function types subtyping).
@@ -463,7 +483,8 @@ Hint Resolve
      elctx_sat_nil elctx_sat_alive elctx_sat_lft_incl elctx_sat_app elctx_sat_refl
      elctx_incl_refl elctx_incl_nil elctx_incl_lft_alive elctx_incl_lft_incl
   : lrust_typing.
-Hint Resolve lctx_lft_alive_external' | 100 : lrust_typing.
+Hint Resolve elctx_sat_cons_weaken elctx_sat_app_weaken_l elctx_sat_app_weaken_r
+             lctx_lft_alive_external' | 100 : lrust_typing.
 
 Hint Opaque elctx_incl elctx_sat lctx_lft_alive lctx_lft_incl : lrust_typing.
 
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index f67534e7e6101ed0ae91bf5637fd2f7fe936affb..469d46d960d848ea844212df40adb83bbbfd2eea 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -89,7 +89,7 @@ Section typing.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply (type_jump [_]); first solve_typing.
+    iApply type_jump; [solve_typing..|].
     iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
   Qed.
 
@@ -101,7 +101,7 @@ Section typing.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply (type_jump [_]); first solve_typing.
+    iApply type_jump; [solve_typing..|].
     iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
   Qed.
 
@@ -113,7 +113,7 @@ Section typing.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
-    iApply (type_jump [_]). solve_typing. rewrite /tctx_incl /=.
+    iApply type_jump; [solve_typing..|]. rewrite /tctx_incl /=.
     iIntros (???) "_ $$". rewrite !tctx_interp_singleton /tctx_elt_interp /=.
     by iIntros "$".
   Qed.
@@ -134,7 +134,7 @@ Section typing.
     iApply type_letalloc_n; [solve_typing| |iIntros (r); simpl_subst].
     { apply (read_shr _ _ _ (cell ty)); solve_typing. }
     iApply type_delete; [solve_typing..|].
-    iApply (type_jump [_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   (* Writing to a cell *)
@@ -186,7 +186,7 @@ Section typing.
     { rewrite /elctx_interp big_opL_singleton. done. }
     iApply type_delete; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
-    iApply (type_jump [ #_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 End typing.
 
diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
index 56d4d9db28ec17517ec8137f2d93d5629a67aac7..819cbba274ef456518620cfbcc91bf0559ee018b 100644
--- a/theories/typing/lib/fake_shared_box.v
+++ b/theories/typing/lib/fake_shared_box.v
@@ -34,6 +34,6 @@ Section fake_shared_box.
             with "[] LFT Hna [Hα Hβ Hαβ] HL Hk [HT]"); last first.
     { by rewrite tctx_interp_singleton tctx_hasty_val. }
     { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
-    iApply (type_jump [_]); simpl; solve_typing.
+    iApply type_jump; simpl; solve_typing.
   Qed.
 End fake_shared_box.
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index dedc8131a23577680d9685c14c14c14d8699dc30..9b7df4c5e8911a3cbb02b72bf73db6322d65c942 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -35,12 +35,12 @@ Section option.
       iApply type_case_uniq; [solve_typing..|].
         constructor; last constructor; last constructor; left.
       + iApply (type_sum_unit (option $ &uniq{α}τ)%T); [solve_typing..|].
-        iApply (type_jump []); solve_typing.
+        iApply type_jump; solve_typing.
       + iApply (type_sum_assign (option $ &uniq{α}τ)%T); [solve_typing..|].
-        iApply (type_jump []); solve_typing.
+        iApply type_jump; solve_typing.
     - iIntros "/= !#". iIntros (k args). inv_vec args. simpl_subst.
       iApply type_delete; [solve_typing..|].
-      iApply (type_jump [_]); solve_typing.
+      iApply type_jump; solve_typing.
   Qed.
 
   Definition option_unwrap_or τ : val :=
@@ -60,10 +60,10 @@ Section option.
       inv_vec p=>o def. simpl_subst.
     iApply type_case_own; [solve_typing|]. constructor; last constructor; last constructor.
     + right. iApply type_delete; [solve_typing..|].
-      iApply (type_jump [_]); solve_typing.
+      iApply type_jump; solve_typing.
     + left. iApply type_letalloc_n; [solve_typing..|]. iIntros (r). simpl_subst.
       iApply (type_delete (Π[uninit _;uninit _;uninit _])); [solve_typing..|].
       iApply type_delete; [solve_typing..|].
-      iApply (type_jump [_]); solve_typing.
+      iApply type_jump; solve_typing.
   Qed.
 End option.
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index 5517099696f5fd0ecba7db2e1c12900d3f272136..45e27b90ecb3f95e66ddf0a6cd1666bfd6196999 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -169,7 +169,7 @@ Section code.
       iNext. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame. iFrame. iLeft.
       rewrite freeable_sz_full_S. iFrame. iExists _. iFrame.  }
     iApply type_delete; [solve_typing..|].
-    iApply (type_jump [ #_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   Definition rc_clone : val :=
@@ -236,7 +236,7 @@ Section code.
       iFrame "Hrc2". iNext. iRight. iExists _, ν, _. iFrame "#∗". }
     { rewrite /elctx_interp big_sepL_singleton. iFrame. }
     iApply type_delete; [solve_typing..|].
-    iApply (type_jump [ #_ ]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   Definition rc_deref : val :=
@@ -279,7 +279,7 @@ Section code.
       iFrame "Hx". iNext. iApply ty_shr_mono; done. }
     { rewrite /elctx_interp big_sepL_singleton. iFrame. }
     iApply type_delete; [solve_typing..|].
-    iApply (type_jump [ #_ ]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   Definition rc_drop ty : val :=
@@ -362,7 +362,7 @@ Section code.
     iApply (type_cont [] [] (λ _, [rcx ◁ box (uninit 1); x ◁ box (option ty)])%TC) ; [solve_typing..| |]; last first.
     { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_delete; [solve_typing..|].
-      iApply (type_jump [_]); solve_typing. }
+      iApply type_jump; solve_typing. }
     iIntros (k). simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid qE) "#LFT Hna HE HL Hk".
@@ -388,7 +388,7 @@ Section code.
         auto with iFrame. }
       iApply (type_sum_memcpy (option _)); [solve_typing..|].
       iApply (type_delete (Π[uninit _; uninit _])); [solve_typing..|].
-      iApply (type_jump []); solve_typing.
+      iApply type_jump; solve_typing.
     - iDestruct "Hproto" as (γ ν q q') "(#Hinv & Hrctok & Hrc● & Hν & _ & _ & Hclose)".
       (* FIXME: linebreaks in "Hclose" do not look as expected. *)
       wp_write. wp_op; intros Hc.
@@ -407,7 +407,7 @@ Section code.
       { rewrite tctx_interp_cons tctx_interp_singleton.
         rewrite !tctx_hasty_val. unlock. iFrame. }
       iApply (type_sum_unit (option ty)); [solve_typing..|].
-      iApply (type_jump []); solve_typing.
+      iApply type_jump; solve_typing.
   Qed.
 
   Definition rc_get_mut : val :=
@@ -435,7 +435,7 @@ Section code.
     iApply (type_cont [] [] (λ r, [rcx ◁ box (uninit 1); x ◁ box (option $ &uniq{α} ty)])%TC) ; [solve_typing..| |]; last first.
     { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_delete; [solve_typing..|].
-      iApply (type_jump [_]); solve_typing. }
+      iApply type_jump; solve_typing. }
     iIntros (k). simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid qE) "#LFT Hna HE HL Hk".
@@ -466,7 +466,7 @@ Section code.
         unlock. iFrame. }
       { rewrite /elctx_interp big_sepL_singleton. done. }
       iApply (type_sum_assign (option (&uniq{_} _))); [solve_typing..|].
-      iApply (type_jump []); solve_typing.
+      iApply type_jump; solve_typing.
     - wp_if. iDestruct "Hc" as "[(% & _)|(% & Hna & Hproto)]".
       { exfalso. subst c. done. }
       iDestruct "Hproto" as (γ ν q q') "(#Hinv & Hrctok & Hrc● & Hν & #Hshr & #Hν† & Hclose2)".
@@ -482,7 +482,7 @@ Section code.
         unlock. iFrame. }
       { rewrite /elctx_interp big_sepL_singleton. done. }
       iApply (type_sum_unit (option (&uniq{_} _))); [solve_typing..|].
-      iApply (type_jump []); solve_typing.
+      iApply type_jump; solve_typing.
   Qed.
 
   (* TODO: * fn make_mut(this: &mut Rc<T>) -> &mut T
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 0aa1cc24af1b3221c60a27e45ee29b4dec5573be..9d04d7c3109b62cf889accd80a3e4a30174ced69 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -103,7 +103,7 @@ Section ref_functions.
       iFrame "∗#". }
     { rewrite /elctx_interp big_sepL_cons big_sepL_singleton. iFrame. }
     iApply type_delete; [solve_typing..|].
-    iApply (type_jump [ #_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   (* Turning a ref into a shared borrow. *)
@@ -139,7 +139,7 @@ Section ref_functions.
     { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
     iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
-    iApply (type_jump [_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   (* Dropping a ref and decrement the count in the corresponding refcell. *)
@@ -200,7 +200,7 @@ Section ref_functions.
     { by rewrite /elctx_interp big_sepL_singleton. }
     iApply type_delete; [solve_typing..|].
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
-    iApply (type_jump [_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   (* Apply a function within the ref, typically for accessing a component. *)
@@ -268,6 +268,6 @@ Section ref_functions.
     iApply type_deref; [solve_typing..|]. iIntros (r'). simpl_subst.
     iApply type_assign; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
-    iApply (type_jump []); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 End ref_functions.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 2854831898b3d3648bb2f7985c2b0b30ee88a991..7ed5f2a2a006e76864f4dd57a39ad6e8c05cbfd6 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -44,7 +44,7 @@ Section refcell_functions.
       - iExists _. rewrite uninit_own. auto.
       - iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. simpl. iFrame. auto. }
     iApply type_delete; [solve_typing..|].
-    iApply (type_jump [ #_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   (* The other direction: getting ownership out of a refcell. *)
@@ -81,7 +81,7 @@ Section refcell_functions.
       - iExists (_::_). rewrite heap_mapsto_vec_cons uninit_own -Hsz. iFrame. auto.
       - iExists vl. iFrame. }
     iApply type_delete; [solve_typing..|].
-    iApply (type_jump [ #_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   Definition refcell_get_mut : val :=
@@ -116,7 +116,7 @@ Section refcell_functions.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iNext. iExists _. rewrite uninit_own. iFrame. }
     iApply type_assign; [solve_typing..|].
-    iApply (type_jump [ #_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   (* Shared borrowing. *)
@@ -150,7 +150,7 @@ Section refcell_functions.
                                     r ◁ box (option (ref α ty))])%TC);
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg]; simpl_subst; last first.
     { iApply type_delete; [solve_typing..|].
-      iApply (type_jump [_]); solve_typing. }
+      iApply type_jump; solve_typing. }
     iApply type_deref; [solve_typing..|].
     iIntros (x' tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -168,7 +168,7 @@ Section refcell_functions.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_unit (option $ ref α ty)); [solve_typing..|]; first last.
-      simpl. iApply (type_jump []); solve_typing.
+      simpl. iApply type_jump; solve_typing.
     - wp_op. wp_write. wp_apply wp_new; [done..|].
       iIntros (lref vl) "(EQ & H† & Hlref)". iDestruct "EQ" as %?%(inj Z.of_nat 2%nat).
       destruct vl as [|?[|?[]]]; try done. wp_let.
@@ -221,7 +221,7 @@ Section refcell_functions.
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_memcpy (option $ ref α ty)); [solve_typing..|].
       simpl. iApply type_delete; [solve_typing..|].
-      iApply (type_jump []); solve_typing.
+      iApply type_jump; solve_typing.
   Qed.
 
   (* Unique borrowing. *)
@@ -257,7 +257,7 @@ Section refcell_functions.
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg];
       simpl_subst; last first.
     { iApply type_delete; [solve_typing..|].
-      iApply (type_jump [_]); solve_typing. }
+      iApply type_jump; solve_typing. }
     iApply type_deref; [solve_typing..|].
     iIntros (x' tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -294,7 +294,7 @@ Section refcell_functions.
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_memcpy (option $ refmut α ty)); [solve_typing..|].
       simpl. iApply type_delete; [solve_typing..|].
-      iApply (type_jump []); solve_typing.
+      iApply type_jump; solve_typing.
     - iMod ("Hclose'" with "[Hlx Hownst Hb] Hna") as "[Hβtok Hna]";
         first by iExists st; iFrame.
       iApply (type_type _ _ _
@@ -303,6 +303,6 @@ Section refcell_functions.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_unit (option $ refmut α ty)); [solve_typing..|].
-      simpl. iApply (type_jump []); solve_typing.
+      simpl. iApply type_jump; solve_typing.
   Qed.
 End refcell_functions.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 85212202feee6bc9f38ba1bc75b2cc9035fb4a8b..22a39c2c4a50ec6486d3fd57f0d428bbe330d11c 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -47,7 +47,7 @@ Section refmut_functions.
     { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
     iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
-    iApply (type_jump [_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   (* Turning a refmut into a unique borrow. *)
@@ -101,7 +101,7 @@ Section refmut_functions.
     { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
     iApply (type_letalloc_1 (&uniq{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
-    iApply (type_jump [_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   (* Dropping a refmut and set the count to 0 in the corresponding refcell. *)
@@ -150,7 +150,7 @@ Section refmut_functions.
     { by rewrite /elctx_interp big_sepL_singleton. }
     iApply type_delete; [solve_typing..|].
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
-    iApply (type_jump [_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   (* Apply a function within the refmut, typically for accessing a component. *)
@@ -220,6 +220,6 @@ Section refmut_functions.
     iApply type_deref; [solve_typing..|]. iIntros (r'). simpl_subst.
     iApply type_assign; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
-    iApply (type_jump []); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 End refmut_functions.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index f1e5a4044f351016efd4a9be4bb326661f36b1b8..95008d7f5e590a7ee213391684cea61476b23c1a 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -44,7 +44,7 @@ Section rwlock_functions.
       - iExists _. rewrite uninit_own. auto.
       - iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. simpl. iFrame. auto. }
     iApply type_delete; [solve_typing..|].
-    iApply (type_jump [ #_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   (* The other direction: getting ownership out of a rwlock.
@@ -80,7 +80,7 @@ Section rwlock_functions.
       - iExists (_::_). rewrite heap_mapsto_vec_cons uninit_own -Hsz. iFrame. auto.
       - iExists vl. iFrame. }
     iApply type_delete; [solve_typing..|].
-    iApply (type_jump [ #_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   Definition rwlock_get_mut : val :=
@@ -115,7 +115,7 @@ Section rwlock_functions.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iNext. iExists _. rewrite uninit_own. iFrame. }
     iApply type_assign; [solve_typing..|].
-    iApply (type_jump [ #_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   (* Acquiring a read lock. *)
@@ -152,11 +152,11 @@ Section rwlock_functions.
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg];
       simpl_subst; last first.
     { iApply type_delete; [solve_typing..|].
-      iApply (type_jump [_]); solve_typing. }
+      iApply type_jump; solve_typing. }
     iApply (type_cont [] [] (λ _, [x ◁ _; x' ◁ _; r ◁ _])%TC);
       [iIntros (loop)|iIntros "/= !#"; iIntros (loop arg); inv_vec arg];
       simpl_subst.
-    { iApply (type_jump []); solve_typing. }
+    { iApply type_jump; solve_typing. }
     iIntros (tid qE) "#LFT Hna HE HL Hk HT".
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
@@ -175,7 +175,7 @@ Section rwlock_functions.
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_unit (option $ rwlockreadguard α ty));
         [solve_typing..|]; first last.
-      simpl. iApply (type_jump []); solve_typing.
+      simpl. iApply type_jump; solve_typing.
     - wp_op. wp_bind (CAS _ _ _).
       iMod (shr_bor_acc_tok with "LFT Hinv Hβtok1") as "[INV Hclose']"; try done.
       iDestruct "INV" as (st') "(Hlx & Hownst & Hst)". revert Hm1.
@@ -228,7 +228,7 @@ Section rwlock_functions.
           iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
         { rewrite {1}/elctx_interp big_sepL_singleton //. }
         iApply (type_sum_assign (option $ rwlockreadguard α ty)); [solve_typing..|].
-        simpl. iApply (type_jump []); solve_typing.
+        simpl. iApply type_jump; solve_typing.
       + iApply (wp_cas_int_fail with "Hlx"); try done. iNext. iIntros "Hlx".
         iMod ("Hclose'" with "[Hlx Hownst Hst]") as "Hβtok1"; first by iExists _; iFrame.
         iModIntro. iApply (wp_if _ false). iNext.
@@ -265,7 +265,7 @@ Section rwlock_functions.
                                     r!!!0 ◁ box (option (rwlockwriteguard α ty))])%TC);
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r];
       simpl_subst; last first.
-    { iApply type_delete; [solve_typing..|]. iApply (type_jump [_]); solve_typing. }
+    { iApply type_delete; [solve_typing..|]. iApply type_jump; solve_typing. }
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_deref; [solve_typing..|].
     iIntros (x' tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
@@ -288,7 +288,7 @@ Section rwlock_functions.
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_unit (option $ rwlockwriteguard α ty));
         [solve_typing..|]; first last.
-      rewrite /option /=. iApply (type_jump [_]); solve_typing.
+      rewrite /option /=. iApply type_jump; solve_typing.
     - iApply (wp_cas_int_suc with "Hlx"). done. iIntros "!> Hlx".
       iMod (own_update with "Hownst") as "[Hownst ?]".
       { by eapply auth_update_alloc, (op_local_update_discrete _ _ writing_st). }
@@ -302,6 +302,6 @@ Section rwlock_functions.
                 tctx_hasty_val' //. iFrame.  iExists _, _. iFrame "∗#". }
       { rewrite {1}/elctx_interp big_sepL_singleton //. }
       iApply (type_sum_assign (option $ rwlockwriteguard α ty)); [solve_typing..|].
-      simpl. iApply (type_jump [_]); solve_typing.
+      simpl. iApply type_jump; solve_typing.
   Qed.
 End rwlock_functions.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 76a8a32bd4036fae443757eba587012e49c533a2..08917456fbbd5185116ea1eb49b95748b0bd1332 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -44,7 +44,7 @@ Section rwlockreadguard_functions.
     { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
     iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
-    iApply (type_jump [_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   (* Dropping a rwlockreadguard and releasing the corresponding lock. *)
@@ -71,7 +71,7 @@ Section rwlockreadguard_functions.
     iApply (type_cont [] [] (λ _, [x ◁ _; x' ◁ _])%TC);
       [iIntros (loop)|iIntros "/= !#"; iIntros (loop arg); inv_vec arg];
       simpl_subst.
-    { iApply (type_jump []); solve_typing. }
+    { iApply type_jump; solve_typing. }
     iIntros (tid qE) "#LFT Hna Hα HL Hk HT".
     rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_cons
             tctx_interp_singleton !tctx_hasty_val.
@@ -133,7 +133,7 @@ Section rwlockreadguard_functions.
       { rewrite /elctx_interp big_sepL_singleton //. }
       iApply type_delete; [solve_typing..|].
       iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
-      iApply (type_jump [_]); solve_typing.
+      iApply type_jump; solve_typing.
     + iApply (wp_cas_int_fail with "Hlx"); try done. iNext. iIntros "Hlx".
       iMod ("Hcloseβ" with "[Hlx H● Hst]") as "Hβ". by iExists _; iFrame.
       iMod ("Hcloseα" with "Hβ") as "HE". iApply (wp_if _ false). iIntros "!> !>".
@@ -142,6 +142,6 @@ Section rwlockreadguard_functions.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val
                 tctx_hasty_val' //. iFrame. iExists _, _, _, _. iFrame "∗#". }
       { rewrite /elctx_interp big_sepL_singleton //. }
-      iApply (type_jump []); solve_typing.
+      iApply type_jump; solve_typing.
   Qed.
 End rwlockreadguard_functions.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 9dc6b47fdf10692838c6532152c7f1b7206af33d..af415324ecfedaf13dee3cbcddf1968925c75de1 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -49,7 +49,7 @@ Section rwlockwriteguard_functions.
     { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
     iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
-    iApply (type_jump [_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   (* Turning a rwlockwriteguard into a unique borrow. *)
@@ -96,7 +96,7 @@ Section rwlockwriteguard_functions.
     { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
     iApply (type_letalloc_1 (&uniq{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
-    iApply (type_jump [_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   (* Drop a rwlockwriteguard and release the lock. *)
@@ -139,6 +139,6 @@ Section rwlockwriteguard_functions.
     { rewrite /elctx_interp big_sepL_singleton //. }
     iApply type_delete; [solve_typing..|].
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
-    iApply (type_jump [_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 End rwlockwriteguard_functions.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 9b4d2ebb7c552ecb11ced0fb6a2dfaac27322083..f65bb4995635e9e14ba75df26ea1e12f65d2765e 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -104,7 +104,7 @@ Section spawn.
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_assign; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
-    iApply (type_jump [_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 
   Definition join : val :=
@@ -129,6 +129,6 @@ Section spawn.
       iDestruct (box_type_incl with "[$Hsub]") as "(_ & Hincl & _)".
       iApply "Hincl". done. }
     iIntros (r); simpl_subst. iApply type_delete; [solve_typing..|].
-    iApply (type_jump [_]); solve_typing.
+    iApply type_jump; solve_typing.
   Qed.
 End spawn.