diff --git a/theories/lang/memcpy.v b/theories/lang/memcpy.v
index e735915caf1063e6cd526a7eddc50264212f53a2..ea0b9359c86f23f0a72764a96ee15f936758a06f 100644
--- a/theories/lang/memcpy.v
+++ b/theories/lang/memcpy.v
@@ -8,7 +8,6 @@ Definition memcpy : val :=
     if: "len" ≤ #0 then #()
     else "dst" <- !"src";;
          "memcpy" ["dst" +â‚— #1 ; "len" - #1 ; "src" +â‚— #1].
-Global Opaque memcpy.
 
 Notation "e1 <-{ n } ! e2" :=
   (memcpy (@cons expr e1%E
diff --git a/theories/lang/new_delete.v b/theories/lang/new_delete.v
index 8c70b067131378e086fb2675777496e870fc29e3..0e2988399e7c60de8a99af34349d248e333d4e60 100644
--- a/theories/lang/new_delete.v
+++ b/theories/lang/new_delete.v
@@ -7,13 +7,11 @@ Definition new : val :=
   λ: ["n"],
     if: "n" ≤ #0 then #((42%positive, 1337):loc)
     else Alloc "n".
-Global Opaque new.
 
 Definition delete : val :=
   λ: ["n"; "loc"],
     if: "n" ≤ #0 then #()
     else Free "n" "loc".
-Global Opaque delete.
 
 Section specs.
   Context `{lrustG Σ}.
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 8af1b8f3e1b8f71fed99d09681e1eecd56668bca..760f8cb1067b2ef3551fea28728faad83e8c6b69 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -46,7 +46,7 @@ Notation "e1 <- e2" := (Write Na1Ord e1%E e2%E)
   (at level 80) : expr_scope.
 Notation "'rec:' f xl := e" := (Rec f%RustB xl%RustB e%E)
   (at level 102, f, xl at level 1, e at level 200) : expr_scope.
-Notation "'rec:' f xl := e" := (RecV f%RustB xl%RustB e%E)
+Notation "'rec:' f xl := e" := (locked (RecV f%RustB xl%RustB e%E))
   (at level 102, f, xl at level 1, e at level 200) : val_scope.
 Notation "e1 +â‚— e2" := (BinOp OffsetOp e1%E e2%E)
   (at level 50, left associativity) : expr_scope.
@@ -58,8 +58,9 @@ notations are otherwise not pretty printed back accordingly. *)
 
 Notation "λ: xl , e" := (Lam xl%RustB e%E)
   (at level 102, xl at level 1, e at level 200) : expr_scope.
-Notation "λ: xl , e" := (LamV xl%RustB e%E)
+Notation "λ: xl , e" := (locked (LamV xl%RustB e%E))
   (at level 102, xl at level 1, e at level 200) : val_scope.
+(* RJ TODO: let the user pick the name of the return continuation. *)
 Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%E
   (only parsing, at level 102, f, xl at level 1, e at level 200) : expr_scope.
 Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%V
diff --git a/theories/lang/spawn.v b/theories/lang/spawn.v
index e62b76ed04653423dcc123fe2feff88a238bb4f7..f30f2db23e14b47bec99b46523266f35a6b217c1 100644
--- a/theories/lang/spawn.v
+++ b/theories/lang/spawn.v
@@ -104,15 +104,14 @@ Lemma join_spec (Ψ : val → iProp Σ) c :
   {{{ join_handle c Ψ }}} join [ #c] {{{ v, RET v; Ψ v }}}.
 Proof.
   iIntros (Φ) "H HΦ". iDestruct "H" as (γf γj) "(Hj & H† & #?)".
-  iLöb as "IH". (* FIXME: Just wp_rec or even simpl unfolds the IH... *)
-  rewrite {1}(lock join). wp_rec.
+  iLöb as "IH". wp_rec.
   wp_bind (!ˢᶜ _)%E. iInv N as "[[_ >Hj']|Hinv]" "Hclose".
   { iExFalso. iCombine "Hj" "Hj'" as "Hj". iDestruct (own_valid with "Hj") as "%".
     auto. }
   iDestruct "Hinv" as (b) "[>Hc Ho]". wp_read. destruct b; last first.
   { iMod ("Hclose" with "[Hc]").
     - iNext. iRight. iExists _. iFrame.
-    - iModIntro. iApply wp_if. iNext. unlock. iApply ("IH" with "Hj H†").
+    - iModIntro. iApply wp_if. iNext. iApply ("IH" with "Hj H†").
       auto. }
   iDestruct "Ho" as (v) "(Hd & HΨ & Hf)".
   iMod ("Hclose" with "[Hj Hf]").
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index fa618fec2f8993dfdd69fd7acbe5102626e12ce2..7b9dc2dd6f629132b439ee78a8efd85567f82bcc 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -17,7 +17,7 @@ Section get_x.
      and without using 'typed_instruction_ty'.  I think that's related to
      the list notation that we added to %TC. *)
   Proof.
-    apply type_fn; try apply _. move=> /= α ret p. inv_vec p=>p. simpl_subst.
+    eapply type_fn; [solve_typing..|]=> /= α ret p. inv_vec p=>p. simpl_subst.
     eapply type_deref; [solve_typing..|by apply read_own_move|done|].
       intros p'; simpl_subst.
     eapply (type_letalloc_1 (&shr{α}int)); [solve_typing..|]=>r. simpl_subst.
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index 5a192f809da6fc3e395cfe399947404dc062f991..967f4735fed4a8198695c9ef4cd0c0b44caefa61 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -15,7 +15,7 @@ Section init_prod.
     typed_instruction_ty [] [] [] init_prod
         (fn([]; int, int) → Π[int;int]).
   Proof.
-    apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>x y. simpl_subst.
+    eapply type_fn; [solve_typing..|]=>- /= [] ret p. inv_vec p=>x y. simpl_subst.
     eapply type_deref; [solve_typing..|apply read_own_move|done|]=>x'. simpl_subst.
     eapply type_deref; [solve_typing..|apply read_own_move|done|]=>y'. simpl_subst.
     eapply (type_new_subtype (Π[uninit 1; uninit 1])); [solve_typing..|].
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 40179b7d550ba9b9c5a4662b740769a0aef5d86a..e7f2c877ab15db7913a315c16f5ab6014edb0606 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -20,7 +20,7 @@ Section lazy_lft.
     typed_instruction_ty [] [] [] lazy_lft
         (fn([]) → unit).
   Proof.
-    apply type_fn; try apply _. move=> /= [] ret p. inv_vec p. simpl_subst.
+    eapply type_fn; [solve_typing..|]=>- /= [] ret p. inv_vec p. simpl_subst.
     eapply (type_newlft []); [solve_typing|]=>α.
     eapply (type_new_subtype (Π[uninit 1;uninit 1])); [solve_typing..|].
       intros t. simpl_subst.
diff --git a/theories/typing/examples/option_as_mut.v b/theories/typing/examples/option_as_mut.v
index 376e6cfe9ff6235ef9f0545ea2be59665c88974b..aef773a7f08a5d881b99fc959fc40fc4d55f4ca8 100644
--- a/theories/typing/examples/option_as_mut.v
+++ b/theories/typing/examples/option_as_mut.v
@@ -18,7 +18,7 @@ Section option_as_mut.
     typed_instruction_ty [] [] [] option_as_mut
         (fn(∀ α, [☀α]; &uniq{α} Σ[unit; τ]) → Σ[unit; &uniq{α}τ]).
   Proof.
-    apply type_fn; try apply _. move=> /= α ret p. inv_vec p=>o. simpl_subst.
+    eapply type_fn; [solve_typing..|]=> /= α ret p. inv_vec p=>o. simpl_subst.
     eapply (type_cont [_] [] (λ r, [o ◁ _; r!!!0 ◁ _])%TC) ; [solve_typing..| |].
     - intros k. simpl_subst.
       eapply type_deref; [solve_typing..|apply read_own_move|done|]=>o'. simpl_subst.
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index 5497184dae1643ef1c1a5d8e769a791fd261f1e6..d0403aab7967084998763538f528f28cde1bec6d 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -19,7 +19,7 @@ Section rebor.
     typed_instruction_ty [] [] [] rebor
         (fn([]; Π[int; int], Π[int; int]) → int).
   Proof.
-    apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>t1 t2. simpl_subst.
+    eapply type_fn; [solve_typing..|]=>- /= [] ret p. inv_vec p=>t1 t2. simpl_subst.
     eapply (type_newlft []). apply _. move=> α.
     eapply (type_letalloc_1 (&uniq{α}Π[int; int])); [solve_typing..|]=>x. simpl_subst.
     eapply type_deref; [solve_typing..|apply read_own_move|done|]=>x'. simpl_subst.
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index f1765799d8cec8d516abc8f2ca0ee11f0c37671a..d682ed72cb7ceefe2da0dc9fff5a5433dd9dea79 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -14,7 +14,7 @@ Section unbox.
     typed_instruction_ty [] [] [] unbox
         (fn(∀ α, [☀α]; &uniq{α}box (Π[int; int])) → &uniq{α} int).
   Proof.
-    apply type_fn; try apply _. move=> /= α ret b. inv_vec b=>b. simpl_subst.
+    eapply type_fn; [solve_typing..|]=> /= α ret b. inv_vec b=>b. simpl_subst.
     eapply type_deref; [solve_typing..|by apply read_own_move|done|].
     intros b'; simpl_subst.
     eapply type_deref_uniq_own; [solve_typing..|]=>bx; simpl_subst.
diff --git a/theories/typing/examples/unwrap_or.v b/theories/typing/examples/unwrap_or.v
index b6a5e1c1ec21776cea8460604f45b2599cab0a70..ccccd9d5907ca64a9fa5002d714b8d0a1b3ac4d7 100644
--- a/theories/typing/examples/unwrap_or.v
+++ b/theories/typing/examples/unwrap_or.v
@@ -15,7 +15,7 @@ Section unwrap_or.
     typed_instruction_ty [] [] [] (unwrap_or Ï„)
         (fn([]; Σ[unit; τ], τ) → τ).
   Proof.
-    apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>o def. simpl_subst.
+    eapply type_fn; [solve_typing..|]=>- /= [] ret p. inv_vec p=>o def. simpl_subst.
     eapply type_case_own; [solve_typing..|]. constructor; last constructor; last constructor.
     + right. eapply type_delete; [solve_typing..|].
       eapply (type_jump [_]); solve_typing.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index d2ce65cb74ae1be16831276ddecaf9d7f9e7bbc7..ce0aeb400448b8856bd75aa9a0a71937b962ba36 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -274,9 +274,11 @@ Section typing.
       apply subst'_is_closed; last done. apply is_closed_of_val.
   Qed.
 
-  Lemma type_rec {A} E L E' fb (argsb : list binder) e
-        (tys : A → vec type (length argsb)) ty
+  Lemma type_rec {A} E L E' fb (argsb : list binder) ef e n
+        (tys : A → vec type n) ty
         T `{!CopyC T, !SendC T} :
+    ef = (funrec: fb argsb := e)%E →
+    n = length argsb →
     Closed (fb :b: "return" :b: argsb +b+ []) e →
     (∀ x (f : val) k (args : vec val (length argsb)),
         typed_body (E' x) [] [k ◁cont([], λ v : vec _ 1, [v!!!0 ◁ box (ty x)])]
@@ -284,9 +286,9 @@ Section typing.
                       zip_with (TCtx_hasty ∘ of_val) args
                                ((λ ty, box ty) <$> vec_to_list (tys x)) ++ T)
                    (subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) →
-    typed_instruction_ty E L T (funrec: fb argsb := e) (fn E' tys ty).
+    typed_instruction_ty E L T ef (fn E' tys ty).
   Proof.
-    iIntros (Hc Hbody) "!# * #LFT $ $ $ #HT". iApply wp_value.
+    iIntros (-> -> Hc Hbody) "!# * #LFT $ $ $ #HT". iApply wp_value.
     { simpl. rewrite ->(decide_left Hc). done. }
     rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
     { simpl. rewrite decide_left. done. }
@@ -297,18 +299,20 @@ Section typing.
     by iApply sendc_change_tid.
   Qed.
 
-  Lemma type_fn {A} E L E' (argsb : list binder) e
-        (tys : A → vec type (length argsb)) ty
+  Lemma type_fn {A} E L E' (argsb : list binder) ef e n
+        (tys : A → vec type n) ty
         T `{!CopyC T, !SendC T} :
+    ef = (funrec: <> argsb := e)%E →
+    n = length argsb →
     Closed ("return" :b: argsb +b+ []) e →
     (∀ x k (args : vec val (length argsb)),
         typed_body (E' x) [] [k ◁cont([], λ v : vec _ 1, [v!!!0 ◁ box (ty x)])]
                    (zip_with (TCtx_hasty ∘ of_val) args
                              ((λ ty, box ty) <$> vec_to_list (tys x)) ++ T)
                    (subst_v (BNamed "return" :: argsb) (k ::: args) e)) →
-    typed_instruction_ty E L T (funrec: <> argsb := e) (fn E' tys ty).
+    typed_instruction_ty E L T ef (fn E' tys ty).
   Proof.
-    intros. apply type_rec; try done. intros. rewrite -typed_body_mono //=.
+    intros. eapply type_rec; try done. intros. rewrite -typed_body_mono //=.
     eapply contains_tctx_incl. by constructor.
   Qed.
 End typing.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index c650b3594538c0f686d08cc180764af83b088823..c6d5452ee971f1b036e74e7683eae1a265ef02f1 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -1,6 +1,7 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import fractional.
+From lrust.lang Require Import proofmode.
 From lrust.lifetime Require Import frac_borrow.
 Set Default Proof Using "Type".
 
@@ -451,6 +452,7 @@ Create HintDb lrust_typing discriminated.
 Create HintDb lrust_typing_merge discriminated.
 
 Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
+Hint Resolve of_val_unlock : lrust_typing.
 Hint Resolve
      lctx_lft_incl_relf lctx_lft_incl_static lctx_lft_incl_local'
      lctx_lft_incl_external'
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 361c1679766e1f7057cd1e33736003b2df68b1d5..ae40afd3c06a74b7f7b96ad51ffb42d6b800258e 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -41,6 +41,7 @@ Section own.
       rewrite /= -Qcmult_plus_distr_l -Z2Qc_inj_add /Z.add. do 3 f_equal. lia.
   Qed.
 
+  (* Make sure 'simpl' doesn't unfold. *)
   Global Opaque freeable_sz.
 
   Program Definition own_ptr (n : nat) (ty : type) :=
@@ -121,7 +122,7 @@ Section own.
   Proof. intros. by apply own_mono. Qed.
   Global Instance own_proper E L :
     Proper (ctx_eq E L ==> eqtype E L ==> eqtype E L) own_ptr.
-  Proof. intros ?? ??? Heq. split; f_equiv; try done; apply Heq. Qed.
+  Proof. intros ??? ??[]; split; by apply own_mono. Qed.
   Lemma own_proper' E L n1 n2 ty1 ty2 :
     ctx_eq E L n1 n2 → eqtype E L ty1 ty2 →
     eqtype E L (own_ptr n1 ty1) (own_ptr n2 ty2).
@@ -282,14 +283,14 @@ Section typing.
   Proof.
     intros. eapply type_new.
     - rewrite /Closed /=. rewrite !andb_True.
-      eauto 100 using is_closed_weaken with set_solver.
+      eauto 10 using is_closed_of_val, is_closed_weaken with set_solver.
     - lia.
     - move=>xv /=.
       assert (subst x xv (x <-{ty.(ty_size)} !p ;; e)%E =
               (xv <-{ty.(ty_size)} !p ;; subst x xv e)%E) as ->.
       { (* TODO : simpl_subst should be able to do this. *)
         unfold subst=>/=. repeat f_equal.
-        - eapply (is_closed_subst []). done. set_solver.
+        - eapply (is_closed_subst []). apply is_closed_of_val. set_solver.
         - by rewrite bool_decide_true.
         - eapply is_closed_subst. done. set_solver. }
       rewrite Nat2Z.id. eapply type_memcpy.
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index a7b050cfd52b22d93dcb11ecd01d9177d4477ff1..90efb8071f51ede048594ca963c6b087b28cfaf1 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -83,7 +83,7 @@ Section typing.
     typed_instruction_ty [] [] [] cell_new
         (fn([]; ty) → cell ty).
   Proof.
-    apply type_fn; [apply _..|]. move=>/= _ ret arg. inv_vec arg=>x. simpl_subst.
+    eapply type_fn; [solve_typing..|]=>- /= _ ret arg. inv_vec arg=>x. simpl_subst.
     eapply (type_jump [_]); first solve_typing.
     iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
   Qed.
@@ -95,7 +95,7 @@ Section typing.
     typed_instruction_ty [] [] [] cell_into_inner
         (fn([]; cell ty) → ty).
   Proof.
-    apply type_fn; [apply _..|]. move=>/= _ ret arg. inv_vec arg=>x. simpl_subst.
+    eapply type_fn; [solve_typing..|]=>-/= _ ret arg. inv_vec arg=>x. simpl_subst.
     eapply (type_jump [_]); first solve_typing.
     iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
   Qed.
@@ -107,7 +107,7 @@ Section typing.
     typed_instruction_ty [] [] [] cell_get_mut
       (fn(∀ α, [☀α]; &uniq{α} (cell ty)) → &uniq{α} ty).
   Proof.
-    apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
+    eapply type_fn; [solve_typing..|]=>- /= α ret arg. inv_vec arg=>x. simpl_subst.
     eapply (type_jump [_]). solve_typing. rewrite /tctx_incl /=.
     iIntros (???) "_ $$". rewrite !tctx_interp_singleton /tctx_elt_interp /=.
     by iIntros "$".
@@ -124,7 +124,7 @@ Section typing.
     typed_instruction_ty [] [] [] (cell_get ty)
         (fn(∀ α, [☀α]; &shr{α} (cell ty)) → ty).
   Proof.
-    apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
+    eapply type_fn; [solve_typing..|]=>- /= α ret arg. inv_vec arg=>x. simpl_subst.
     eapply type_deref; [solve_typing..|apply read_own_move|done|]=>x'. simpl_subst.
     eapply type_letalloc_n; [solve_typing..| |solve_typing|intros r; simpl_subst].
     { apply (read_shr _ _ _ (cell ty)); solve_typing. }
@@ -144,7 +144,7 @@ Section typing.
     typed_instruction_ty [] [] [] (cell_set ty)
         (fn(∀ α, [☀α]; &shr{α} cell ty, ty) → unit).
   Proof.
-    apply type_fn; try apply _. move=> /= α ret arg. inv_vec arg=>c x. simpl_subst.
+    eapply type_fn; [solve_typing..|]=>- /= α ret arg. inv_vec arg=>c x. simpl_subst.
     eapply type_deref; [solve_typing..|by apply read_own_move|done|].
     intros d. simpl_subst.
     eapply type_let with (T1 := [d ◁ _; x ◁ _]%TC)
diff --git a/theories/typing/unsafe/refcell/ref_code.v b/theories/typing/unsafe/refcell/ref_code.v
index ac08fb9dadd677ec76c972688d96d7dd314ccb55..3c816d249b49982bf6579d7d7ef23b829480832d 100644
--- a/theories/typing/unsafe/refcell/ref_code.v
+++ b/theories/typing/unsafe/refcell/ref_code.v
@@ -59,7 +59,7 @@ Section ref_functions.
       (fn (fun '(α, β) => [☀α; ☀β])%EL (fun '(α, β) => [# &shr{α}(ref β ty)]%T)
                                        (fun '(α, β) => ref β ty)%T).
   Proof.
-    apply type_fn; [apply _..|]. move=>/= [α β] ret arg. inv_vec arg=>x. simpl_subst.
+    eapply type_fn; [solve_typing..|]. move=>/= [α β] ret arg. inv_vec arg=>x. simpl_subst.
     eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
     iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -124,7 +124,7 @@ Section ref_functions.
           (fun '(α, β) => [# &shr{α}(ref β ty)]%T)
           (fun '(α, β) => &shr{α}ty)%T).
   Proof.
-    apply type_fn; [apply _..|]. move=>/= [α β] ret arg. inv_vec arg=>x. simpl_subst.
+    eapply type_fn; [solve_typing..|]. move=>/= [α β] ret arg. inv_vec arg=>x. simpl_subst.
     eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
     iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -162,7 +162,7 @@ Section ref_functions.
     typed_instruction_ty [] [] [] ref_drop
       (fn (fun α => [☀α])%EL (fun α => [# ref α ty])  (fun α => unit)).
   Proof.
-    apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
+    eapply type_fn; [solve_typing..|]=>- /= α ret arg. inv_vec arg=>x. simpl_subst.
     iIntros "!# * #LFT Hna Hα HL Hk Hx".
     rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_singleton tctx_hasty_val.
     destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hx Hx†]".
diff --git a/theories/typing/unsafe/refcell/refcell_code.v b/theories/typing/unsafe/refcell/refcell_code.v
index fa185e27664170c2c25f383903b3be0cfba20f5e..45f49ae15d95fc3450a323f2130f9a368cb5f5ef 100644
--- a/theories/typing/unsafe/refcell/refcell_code.v
+++ b/theories/typing/unsafe/refcell/refcell_code.v
@@ -23,7 +23,7 @@ Section refcell_functions.
     typed_instruction_ty [] [] [] (refcell_new ty)
         (fn (λ _, []) (λ _, [# ty]) (λ _:(), refcell ty)).
   Proof.
-    apply type_fn; [apply _..|]. move=>/= _ ret arg. inv_vec arg=>x. simpl_subst.
+    eapply type_fn; [solve_typing..|]=>-/= _ ret arg. inv_vec arg=>x. simpl_subst.
     eapply type_new; [solve_typing..|].
     iIntros (r) "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite (Nat2Z.id (S ty.(ty_size))) tctx_interp_cons
@@ -58,7 +58,7 @@ Section refcell_functions.
     typed_instruction_ty [] [] [] (refcell_into_inner ty)
         (fn (λ _, []) (λ _, [# refcell ty]) (λ _:(), ty)).
   Proof.
-    apply type_fn; [apply _..|]. move=>/= _ ret arg. inv_vec arg=>x. simpl_subst.
+    eapply type_fn; [solve_typing..|]=>- /= _ ret arg. inv_vec arg=>x. simpl_subst.
     eapply type_new; [solve_typing..|].
     iIntros (r) "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite (Nat2Z.id (ty.(ty_size))) tctx_interp_cons
@@ -91,7 +91,7 @@ Section refcell_functions.
     typed_instruction_ty [] [] [] refcell_get_mut
         (fn (λ α, [☀α])%EL (λ α, [# &uniq{α} (refcell ty)])%T (λ α, &uniq{α} ty)%T).
   Proof.
-    apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
+    eapply type_fn; [solve_typing..|]=>- /= α ret arg. inv_vec arg=>x. simpl_subst.
     eapply type_deref; [solve_typing..|by eapply read_own_move|done|]=>x'. simpl_subst.
     iIntros "!# * #LFT Hna HE HL HC HT".
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -140,7 +140,7 @@ Section refcell_functions.
     typed_instruction_ty [] [] [] refcell_try_borrow
         (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, Σ[ref α ty; unit])%T).
   Proof.
-    apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
+    eapply type_fn; [solve_typing..|]=>- /= α ret arg. inv_vec arg=>x. simpl_subst.
     eapply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} refcell ty);
                                     r!!!0 ◁ box Σ[ref α ty; unit]])%TC);
       [solve_typing..|intros k|move=>/= k arg; inv_vec arg=>r]; simpl_subst; last first.
@@ -245,7 +245,7 @@ Section refcell_functions.
     typed_instruction_ty [] [] [] refcell_try_borrow_mut
         (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, Σ[refmut α ty; unit])%T).
   Proof.
-    apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
+    eapply type_fn; [solve_typing..|]=>- /= α ret arg. inv_vec arg=>x. simpl_subst.
     eapply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} refcell ty);
                                     r!!!0 ◁ box Σ[refmut α ty; unit]])%TC);
       [solve_typing..|intros k|move=>/= k arg; inv_vec arg=>r]; simpl_subst; last first.
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
index e3e528509b0b42e3d578f1975ed676a98760d888..88819e742f88526dad8951839e0418ebe072613f 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/unsafe/refcell/refmut_code.v
@@ -26,7 +26,7 @@ Section refmut_functions.
           (fun '(α, β) => [# &shr{α}(refmut β ty)]%T)
           (fun '(α, β) => &shr{α}ty)%T).
   Proof.
-    apply type_fn; [apply _..|]. move=>/= [α β] ret arg. inv_vec arg=>x. simpl_subst.
+    eapply type_fn; [solve_typing..|]. move=> /= [α β] ret arg. inv_vec arg=>x. simpl_subst.
     eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
     iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -69,7 +69,7 @@ Section refmut_functions.
           (fun '(α, β) => [# &uniq{α}(refmut β ty)]%T)
           (fun '(α, β) => &uniq{α}ty)%T).
   Proof.
-    apply type_fn; [apply _..|]. move=>/= [α β] ret arg. inv_vec arg=>x. simpl_subst.
+    eapply type_fn; [solve_typing..|]. move=>/= [α β] ret arg. inv_vec arg=>x. simpl_subst.
     eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
     iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -124,7 +124,7 @@ Section refmut_functions.
     typed_instruction_ty [] [] [] refmut_drop
       (fn(∀ α, [☀α]; refmut α ty) → unit).
   Proof.
-    apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
+    eapply type_fn; [solve_typing..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
     iIntros "!# * #LFT Hna Hα HL Hk Hx".
     rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_singleton tctx_hasty_val.
     destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hx Hx†]".
diff --git a/theories/typing/unsafe/spawn.v b/theories/typing/unsafe/spawn.v
index 20eac315935c5a4518c3a5f10c4def964f2476d9..38fef78a0315099bf7325652d64b652d1128b74d 100644
--- a/theories/typing/unsafe/spawn.v
+++ b/theories/typing/unsafe/spawn.v
@@ -20,7 +20,7 @@ Section spawn.
     typed_instruction_ty [] [] [] spawn
         (fn([]; fn([] ; envty) → unit, envty) → unit).
   Proof. (* FIXME: typed_instruction_ty is not used for printing. *)
-    apply type_fn; [apply _..|]=>_ ret /= arg. inv_vec arg=>f env. simpl_subst.
+    eapply type_fn; [solve_typing..|]=>- _ ret /= arg. inv_vec arg=>f env. simpl_subst.
     eapply type_deref; [solve_typing..|exact: read_own_move|done|].
     move=>f'. simpl_subst.
     eapply type_let with (T1 := [f' ◁ _; env ◁ _]%TC)