diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 7cb39d571e118e262c9f4d8d158b5b353bf78ed3..cb2c8deff443538d4aed5bca4637d81b73e33535 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -23,10 +23,9 @@ End bool.
 Section typing.
   Context `{typeG Σ}.
 
-  Lemma type_bool_instr (b : Datatypes.bool) E L :
-    typed_instruction_ty E L [] #b bool.
+  Lemma type_bool_instr (b : Datatypes.bool) : typed_val #b bool.
   Proof.
-    iIntros (tid qE) "_ $ $ $ _". wp_value.
+    iIntros (E L tid qE) "_ $ $ $ _". wp_value.
     rewrite tctx_interp_singleton tctx_hasty_val. by destruct b.
   Qed.
 
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index e6c440cd240f8a43dac0be026d0d269256f3623d..e63a253c79d28aabc8e5cff7d7feb9ef5ebf5bc4 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -12,13 +12,12 @@ Section get_x.
        delete [ #1; "p"] ;; "return" ["r"].
 
   Lemma get_x_type :
-    typed_instruction_ty [] [] [] get_x
-        (fn(∀ α, [☀α]; &uniq{α} Π[int; int]) → &shr{α} int).
+    typed_val get_x (fn(∀ α, [☀α]; &uniq{α} Π[int; int]) → &shr{α} int).
   (* FIXME: The above is pretty-printed with some explicit scope annotations,
      and without using 'typed_instruction_ty'.  I think that's related to
      the list notation that we added to %TC. *)
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret p).
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret p).
     inv_vec p=>p. simpl_subst.
     iApply type_deref; [solve_typing..|by apply read_own_move|done|].
       iIntros (p'); simpl_subst.
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index c307f3a96b79465d976a3919be63f2bb45f8e4c1..5b0d3bc1f1da47639d92492407d5cc548ae781de 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -13,10 +13,9 @@ Section init_prod.
        delete [ #1; "x"] ;; delete [ #1; "y"] ;; "return" ["r"].
 
   Lemma init_prod_type :
-    typed_instruction_ty [] [] [] init_prod
-        (fn([]; int, int) → Π[int;int]).
+    typed_val init_prod (fn([]; int, int) → Π[int;int]).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
       inv_vec p=>x y. simpl_subst.
     iApply type_deref; [solve_typing..|apply read_own_move|done|]. iIntros (x'). simpl_subst.
     iApply type_deref; [solve_typing..|apply read_own_move|done|]. iIntros (y'). simpl_subst.
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 16869ee69712c32d5bfd92e7d116f4923b79b893..6960ab838a64967486c1b99988fab21b7b6edeac 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -18,10 +18,9 @@ Section lazy_lft.
       Endlft;; delete [ #2; "t"];; delete [ #1; "f"];; delete [ #1; "g"];; "return" ["r"].
 
   Lemma lazy_lft_type :
-    typed_instruction_ty [] [] [] lazy_lft
-        (fn([]) → unit).
+    typed_val lazy_lft (fn([]) → unit).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
       inv_vec p. simpl_subst.
     iApply (type_newlft []). iIntros (α).
     iApply (type_new_subtype (Π[uninit 1;uninit 1])); [solve_typing..|].
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index 67a7632b7425b121155b2f0aa2d43c6fc1be830b..9ec1c0c88f25d79b30c8f21bea0b8a8d13ea865f 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -17,10 +17,9 @@ Section rebor.
                  delete [ #1; "x"] ;; "return" ["r"].
 
   Lemma rebor_type :
-    typed_instruction_ty [] [] [] rebor
-        (fn([]; Π[int; int], Π[int; int]) → int).
+    typed_val rebor (fn([]; Π[int; int], Π[int; int]) → int).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
        inv_vec p=>t1 t2. simpl_subst.
     iApply (type_newlft []). iIntros (α).
     iApply (type_letalloc_1 (&uniq{α}Π[int; int])); [solve_typing..|]. iIntros (x). simpl_subst.
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index 4c99656ee226f1290478b9d0dd46f7e862d09328..78a3b34bb03cbbe912d21e8341e296fc7b5648b3 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -12,10 +12,9 @@ Section unbox.
        delete [ #1; "b"] ;; "return" ["r"].
 
   Lemma ubox_type :
-    typed_instruction_ty [] [] [] unbox
-        (fn(∀ α, [☀α]; &uniq{α}box (Π[int; int])) → &uniq{α} int).
+    typed_val unbox (fn(∀ α, [☀α]; &uniq{α}box (Π[int; int])) → &uniq{α} int).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret b).
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret b).
       inv_vec b=>b. simpl_subst.
     iApply type_deref; [solve_typing..|by apply read_own_move|done|].
     iIntros (b'); simpl_subst.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index fd21063ae06fa0fd8375fc1ccf339bd1e980c8a6..f87c9ac00fcc9ca0cfcc3f8c16bb94ecc88d9429 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -22,10 +22,9 @@ End int.
 Section typing.
   Context `{typeG Σ}.
 
-  Lemma type_int_instr (z : Z) E L :
-    typed_instruction_ty E L [] #z int.
+  Lemma type_int_instr (z : Z) : typed_val #z int.
   Proof.
-    iIntros (tid qE) "_ $ $ $ _". wp_value.
+    iIntros (E L tid qE) "_ $ $ $ _". wp_value.
     by rewrite tctx_interp_singleton tctx_hasty_val.
   Qed.
 
diff --git a/theories/typing/option.v b/theories/typing/option.v
index 86ac155dde5763b133de5837391ceae2d5d1f806..7aea21c9fbdea20b00fc61908941eca7dcf5b5a1 100644
--- a/theories/typing/option.v
+++ b/theories/typing/option.v
@@ -18,10 +18,10 @@ Section option.
         delete [ #1; "o"];; "return" ["r"].
 
   Lemma option_as_mut_type Ï„ :
-    typed_instruction_ty [] [] [] option_as_mut
-        (fn(∀ α, [☀α]; &uniq{α} (option τ)) → option (&uniq{α}τ)).
+    typed_val
+      option_as_mut (fn(∀ α, [☀α]; &uniq{α} (option τ)) → option (&uniq{α}τ)).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret p).
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret p).
       inv_vec p=>o. simpl_subst.
     iApply (type_cont [_] [] (λ r, [o ◁ _; r!!!0 ◁ _])%TC) ; [solve_typing..| |].
     - iIntros (k). simpl_subst.
@@ -50,10 +50,9 @@ Section option.
         "return" ["r"]].
 
   Lemma option_unwrap_or_type Ï„ :
-    typed_instruction_ty [] [] [] (option_unwrap_or Ï„)
-        (fn([]; option τ, τ) → τ).
+    typed_val (option_unwrap_or τ) (fn([]; option τ, τ) → τ).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
       inv_vec p=>o def. simpl_subst.
     iApply type_case_own; [solve_typing|]. constructor; last constructor; last constructor.
     + right. iApply type_delete; [solve_typing..|].
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 2c52aba10fe7f52b61071d0233f48ff44c6a1481..bfb27a38dda5405bc9d607a92dfbfe25ec7b41df 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -79,8 +79,10 @@ Section typing.
   Global Arguments typed_read _%EL _%LL _%T _%T _%T.
 End typing.
 
-Notation typed_instruction_ty E L T1 e ty :=
-  (typed_instruction E L T1 e (λ v : val, [v ◁ ty%list%T]%TC)).
+Notation typed_instruction_ty E L T e ty :=
+  (typed_instruction E L T e (λ v : val, [v ◁ ty%list%T]%TC)).
+
+Notation typed_val e ty := (∀ E L, typed_instruction_ty E L [] e ty).
 
 Section typing_rules.
   Context `{typeG Σ}.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index e5ca263bafce794e3983ccacb2afe70b22b2b9b3..eda8bb99162e6104b8c10f925b58bc00e81e45cc 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -23,11 +23,10 @@ Proof. solve_inG. Qed.
 Section type_soundness.
   Definition exit_cont : val := λ: [<>], #().
 
-  Definition main_type `{typeG Σ} :=
-    (fn([]) → unit)%T.
+  Definition main_type `{typeG Σ} := (fn([]) → unit)%T.
 
   Theorem type_soundness `{typePreG Σ} (main : val) σ t :
-    (∀ `{typeG Σ}, typed_instruction_ty [] [] [] main main_type) →
+    (∀ `{typeG Σ}, typed_val main main_type) →
     rtc step ([main [exit_cont]%E], ∅) (t, σ) →
     nonracing_threadpool t σ ∧
     (∀ e, e ∈ t → is_Some (to_val e) ∨ reducible e σ).
@@ -40,7 +39,7 @@ Section type_soundness.
     iMod lft_init as (?) "#LFT". done.
     iMod na_alloc as (tid) "Htl". set (Htype := TypeG _ _ _ _ _).
     wp_bind (of_val main). iApply (wp_wand with "[Htl]").
-    iApply (Hmain _ $! tid 1%Qp with "LFT Htl [] [] []").
+    iApply (Hmain _ [] [] $! tid 1%Qp with "LFT Htl [] [] []").
     { by rewrite /elctx_interp big_sepL_nil. }
     { by rewrite /llctx_interp big_sepL_nil. }
     { by rewrite tctx_interp_nil. }
@@ -61,7 +60,7 @@ End type_soundness.
 (* Soundness theorem when no other CMRA is needed. *)
 
 Theorem type_soundness_closed (main : val) σ t :
-  (∀ `{typeG typeΣ}, typed_instruction_ty [] [] [] main main_type) →
+  (∀ `{typeG typeΣ}, typed_val main main_type) →
   rtc step ([main [exit_cont]%E], ∅) (t, σ) →
   nonracing_threadpool t σ ∧
   (∀ e, e ∈ t → is_Some (to_val e) ∨ reducible e σ).
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index 76dcf3236685287540b40a30f06eb06432d4dbe8..a0063c1a4f4e91d6412ef21a36fc0b092040da9d 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -26,7 +26,8 @@ Section cell.
 
   Global Instance cell_ne : NonExpansive cell.
   Proof.
-    constructor; solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
+    constructor;
+      solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
   Qed.
 
   Global Instance cell_mono E L : Proper (eqtype E L ==> subtype E L) cell.
@@ -84,11 +85,10 @@ Section typing.
   Definition cell_new : val := funrec: <> ["x"] := "return" ["x"].
 
   Lemma cell_new_type ty :
-    typed_instruction_ty [] [] [] cell_new
-        (fn([]; ty) → cell ty).
+    typed_val cell_new (fn([]; ty) → cell ty).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (_ ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_jump [_]); first solve_typing.
     iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
   Qed.
@@ -97,11 +97,10 @@ Section typing.
   Definition cell_into_inner : val := funrec: <> ["x"] := "return" ["x"].
 
   Lemma cell_into_inner_type ty :
-    typed_instruction_ty [] [] [] cell_into_inner
-        (fn([]; cell ty) → ty).
+    typed_val cell_into_inner (fn([]; cell ty) → ty).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (_ ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_jump [_]); first solve_typing.
     iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
   Qed.
@@ -110,11 +109,10 @@ Section typing.
     funrec: <> ["x"] := "return" ["x"].
 
   Lemma cell_get_mut_type ty :
-    typed_instruction_ty [] [] [] cell_get_mut
-      (fn(∀ α, [☀α]; &uniq{α} (cell ty)) → &uniq{α} ty).
+    typed_val cell_get_mut (fn(∀ α, [☀α]; &uniq{α} (cell ty)) → &uniq{α} ty).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_jump [_]). solve_typing. rewrite /tctx_incl /=.
     iIntros (???) "_ $$". rewrite !tctx_interp_singleton /tctx_elt_interp /=.
     by iIntros "$".
@@ -128,11 +126,10 @@ Section typing.
       delete [ #1; "x"];; "return" ["r"].
 
   Lemma cell_get_type `(!Copy ty) :
-    typed_instruction_ty [] [] [] (cell_get ty)
-        (fn(∀ α, [☀α]; &shr{α} (cell ty)) → ty).
+    typed_val (cell_get ty) (fn(∀ α, [☀α]; &shr{α} (cell ty)) → ty).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing|apply read_own_move|done|]. iIntros (x'). simpl_subst.
     iApply type_letalloc_n; [solve_typing| |iIntros (r); simpl_subst].
     { apply (read_shr _ _ _ (cell ty)); solve_typing. }
@@ -149,11 +146,10 @@ Section typing.
       delete [ #1; "c"] ;; delete [ #ty.(ty_size); "x"] ;; "return" ["r"].
 
   Lemma cell_replace_type ty :
-    typed_instruction_ty [] [] [] (cell_replace ty)
-        (fn(∀ α, [☀α]; &shr{α} cell ty, ty) → ty).
+    typed_val (cell_replace ty) (fn(∀ α, [☀α]; &shr{α} cell ty, ty) → ty).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
-      inv_vec arg=>c x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ret arg). inv_vec arg=>c x. simpl_subst.
     iApply type_deref; [solve_typing|exact: read_own_move|done|]. iIntros (c'); simpl_subst.
     iApply type_new; [solve_typing..|]. iIntros (r); simpl_subst.
     (* Drop to Iris level. *)
diff --git a/theories/typing/unsafe/refcell/ref_code.v b/theories/typing/unsafe/refcell/ref_code.v
index f740e8eb69c75462fed2fed39f55931e81a69af8..7cc4b5147952ae6f750ca4fbaa0329686f2a4bf0 100644
--- a/theories/typing/unsafe/refcell/ref_code.v
+++ b/theories/typing/unsafe/refcell/ref_code.v
@@ -55,12 +55,12 @@ Section ref_functions.
   (* FIXME : using λ instead of fun triggers an anomaly.
      See: https://coq.inria.fr/bugs/show_bug.cgi?id=5326 *)
   Lemma ref_clone_type ty :
-    typed_instruction_ty [] [] [] ref_clone
+    typed_val ref_clone
       (fn (fun '(α, β) => [☀α; ☀β])%EL (fun '(α, β) => [# &shr{α}(ref β ty)]%T)
                                        (fun '(α, β) => ref β ty)%T).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([α β] ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
     iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -116,13 +116,13 @@ Section ref_functions.
       delete [ #1; "x"];; "return" ["r"].
 
   Lemma ref_deref_type ty :
-    typed_instruction_ty [] [] [] ref_deref
+    typed_val ref_deref
       (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
           (fun '(α, β) => [# &shr{α}(ref β ty)]%T)
           (fun '(α, β) => &shr{α}ty)%T).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([α β] ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
     iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -156,10 +156,10 @@ Section ref_functions.
       let: "r" := new [ #0] in "return" ["r"].
 
   Lemma ref_drop_type ty :
-    typed_instruction_ty [] [] [] ref_drop (fn(∀ α, [☀α]; ref α ty) → unit).
+    typed_val ref_drop (fn(∀ α, [☀α]; ref α ty) → unit).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
     iIntros (tid qE) "#LFT Hna Hα HL Hk Hx".
     rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_singleton tctx_hasty_val.
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
@@ -220,11 +220,11 @@ Section ref_functions.
       "return" ["ref"].
 
   Lemma ref_map_type ty1 ty2 envty E :
-    typed_instruction_ty [] [] [] ref_map
+    typed_val ref_map
       (fn(∀ β, [☀β] ++ E; ref β ty1, fn(∀ α, [☀α] ++ E; envty, &shr{α}ty1) → &shr{α}ty2, envty)
        → ref β ty2).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
        inv_vec arg=>ref f env. simpl_subst.
     iIntros (tid qE) "#LFT Hna HE HL Hk HT".
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -265,7 +265,7 @@ Section ref_functions.
     iApply type_deref; [solve_typing..|by apply read_own_move|done|].
       iIntros (x'). simpl_subst.
     iApply type_deref; [solve_typing..|by apply read_own_move|done|].
-       iIntros (f'). simpl_subst.
+      iIntros (f'). simpl_subst.
     iApply type_letalloc_1; [solve_typing..|]. iIntros (x). simpl_subst.
     iApply (type_letcall); [simpl; solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_deref; [solve_typing|by eapply read_own_move|done|].
diff --git a/theories/typing/unsafe/refcell/refcell_code.v b/theories/typing/unsafe/refcell/refcell_code.v
index 8d1d4d4ef25c80fbc415703ba72db809a58e3600..7e8d244db936975e9ba2d7ed4f22f052cd1a9a05 100644
--- a/theories/typing/unsafe/refcell/refcell_code.v
+++ b/theories/typing/unsafe/refcell/refcell_code.v
@@ -20,11 +20,11 @@ Section refcell_functions.
        delete [ #ty.(ty_size) ; "x"];; "return" ["r"].
 
   Lemma refcell_new_type ty :
-    typed_instruction_ty [] [] [] (refcell_new ty)
-        (fn (λ _, []) (λ _, [# ty]) (λ _:(), refcell ty)).
+    typed_val (refcell_new ty)
+      (fn (λ _, []) (λ _, [# ty]) (λ _:(), refcell ty)).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (_ ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|].
     iIntros (r tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite (Nat2Z.id (S ty.(ty_size))) tctx_interp_cons
@@ -58,11 +58,11 @@ Section refcell_functions.
        delete [ #(S ty.(ty_size)) ; "x"];; "return" ["r"].
 
   Lemma refcell_into_inner_type ty :
-    typed_instruction_ty [] [] [] (refcell_into_inner ty)
-        (fn (λ _, []) (λ _, [# refcell ty]) (λ _:(), ty)).
+    typed_val (refcell_into_inner ty)
+                   (fn (λ _, []) (λ _, [# refcell ty]) (λ _:(), ty)).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (_ ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|].
     iIntros (r tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite (Nat2Z.id (ty.(ty_size))) tctx_interp_cons
@@ -93,11 +93,11 @@ Section refcell_functions.
       "return" ["x"].
 
   Lemma refcell_get_mut_type ty :
-    typed_instruction_ty [] [] [] refcell_get_mut
+    typed_val refcell_get_mut
         (fn (λ α, [☀α])%EL (λ α, [# &uniq{α} (refcell ty)])%T (λ α, &uniq{α} ty)%T).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|by eapply read_own_move|done|].
       iIntros (x'). simpl_subst.
     iIntros (tid qE) "#LFT Hna HE HL HC HT".
@@ -144,11 +144,11 @@ Section refcell_functions.
         delete [ #1; "x"];; "return" ["r"].
 
   Lemma refcell_try_borrow_type ty :
-    typed_instruction_ty [] [] [] refcell_try_borrow
+    typed_val refcell_try_borrow
         (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, option (ref α ty))%T).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} refcell ty);
                                     r!!!0 ◁ box (option (ref α ty))])%TC);
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r]; simpl_subst; last first.
@@ -251,11 +251,11 @@ Section refcell_functions.
         delete [ #1; "x"];; "return" ["r"].
 
   Lemma refcell_try_borrow_mut_type ty :
-    typed_instruction_ty [] [] [] refcell_try_borrow_mut
+    typed_val refcell_try_borrow_mut
         (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, option (refmut α ty))%T).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} refcell ty);
                                     r!!!0 ◁ box (option (refmut α ty))]%TC));
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r];
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
index e4102353a35f10914972f04c7f7a1a7af2aab94d..06f36675a40d11419e58fca60adc1ad8134c6a20 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/unsafe/refcell/refmut_code.v
@@ -19,13 +19,13 @@ Section refmut_functions.
       delete [ #1; "x"];; "return" ["r"].
 
   Lemma refmut_deref_type ty :
-    typed_instruction_ty [] [] [] refmut_deref
+    typed_val refmut_deref
       (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
           (fun '(α, β) => [# &shr{α}(refmut β ty)]%T)
           (fun '(α, β) => &shr{α}ty)%T).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([α β] ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
     iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -61,13 +61,13 @@ Section refmut_functions.
       delete [ #1; "x"];; "return" ["r"].
 
   Lemma refmut_derefmut_type ty :
-    typed_instruction_ty [] [] [] refmut_derefmut
+    typed_val refmut_derefmut
       (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
           (fun '(α, β) => [# &uniq{α}(refmut β ty)]%T)
           (fun '(α, β) => &uniq{α}ty)%T).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([α β] ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
     iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -117,10 +117,10 @@ Section refmut_functions.
       let: "r" := new [ #0] in "return" ["r"].
 
   Lemma refmut_drop_type ty :
-    typed_instruction_ty [] [] [] refmut_drop (fn(∀ α, [☀α]; refmut α ty) → unit).
+    typed_val refmut_drop (fn(∀ α, [☀α]; refmut α ty) → unit).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
     iIntros (tid qE) "#LFT Hna Hα HL Hk Hx".
     rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_singleton tctx_hasty_val.
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
@@ -170,14 +170,14 @@ Section refmut_functions.
       "return" ["ref"].
 
   Lemma refmut_map_type ty1 ty2 envty E :
-    typed_instruction_ty [] [] [] refmut_map
+    typed_val refmut_map
       (fn(∀ β, [☀β] ++ E; refmut β ty1,
                           fn(∀ α, [☀α] ++ E; envty, &uniq{α} ty1) → &uniq{α} ty2,
                           envty)
        → refmut β ty2).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
-       inv_vec arg=>ref f env. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ret arg). inv_vec arg=>ref f env. simpl_subst.
     iIntros (tid qE) "#LFT Hna HE HL Hk HT".
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "(Href & Hf & Henv)".
diff --git a/theories/typing/unsafe/rwlock/rwlock_code.v b/theories/typing/unsafe/rwlock/rwlock_code.v
index 46aa4d6fc62a083c1fcc0fdfc453bcc0ef7e3aa9..9aa1f3504a273e2342c053e8e91875bced7c561c 100644
--- a/theories/typing/unsafe/rwlock/rwlock_code.v
+++ b/theories/typing/unsafe/rwlock/rwlock_code.v
@@ -20,11 +20,10 @@ Section rwlock_functions.
        delete [ #ty.(ty_size) ; "x"];; "return" ["r"].
 
   Lemma rwlock_new_type ty :
-    typed_instruction_ty [] [] [] (rwlock_new ty)
-        (fn (λ _, []) (λ _, [# ty]) (λ _:(), rwlock ty)).
+    typed_val (rwlock_new ty) (fn (λ _, []) (λ _, [# ty]) (λ _:(), rwlock ty)).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (_ ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|].
     iIntros (r tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite (Nat2Z.id (S ty.(ty_size))) tctx_interp_cons
@@ -57,11 +56,11 @@ Section rwlock_functions.
        delete [ #(S ty.(ty_size)) ; "x"];; "return" ["r"].
 
   Lemma rwlock_into_inner_type ty :
-    typed_instruction_ty [] [] [] (rwlock_into_inner ty)
+    typed_val (rwlock_into_inner ty)
         (fn (λ _, []) (λ _, [# rwlock ty]) (λ _:(), ty)).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (_ ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|].
     iIntros (r tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite (Nat2Z.id (ty.(ty_size))) tctx_interp_cons
@@ -92,11 +91,11 @@ Section rwlock_functions.
       "return" ["x"].
 
   Lemma rwlock_get_mut_type ty :
-    typed_instruction_ty [] [] [] rwlock_get_mut
+    typed_val rwlock_get_mut
         (fn (λ α, [☀α])%EL (λ α, [# &uniq{α} (rwlock ty)])%T (λ α, &uniq{α} ty)%T).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|by eapply read_own_move|done|].
       iIntros (x'). simpl_subst.
     iIntros (tid qE) "#LFT Hna HE HL HC HT".
@@ -142,12 +141,12 @@ Section rwlock_functions.
         delete [ #1; "x"];; "return" ["r"].
 
   Lemma rwlock_try_read_type ty :
-    typed_instruction_ty [] [] [] rwlock_try_read
+    typed_val rwlock_try_read
         (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(rwlock ty)]%T)
             (λ α, option (rwlockreadguard α ty))%T).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} rwlock ty);
                                     r!!!0 ◁ box (option (rwlockreadguard α ty))])%TC);
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r];
@@ -260,12 +259,12 @@ Section rwlock_functions.
         delete [ #1; "x"];; "return" ["r"].
 
   Lemma rwlock_try_write_type ty :
-    typed_instruction_ty [] [] [] rwlock_try_write
+    typed_val rwlock_try_write
         (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(rwlock ty)]%T)
             (λ α, option (rwlockwriteguard α ty))%T).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} rwlock ty);
                                     r!!!0 ◁ box (option (rwlockwriteguard α ty))])%TC);
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r];
diff --git a/theories/typing/unsafe/rwlock/rwlockreadguard_code.v b/theories/typing/unsafe/rwlock/rwlockreadguard_code.v
index f7c493bb2017641e5df59b573955db77b0b9489b..659d74d159c4c01b586bf242e22a32360c07df86 100644
--- a/theories/typing/unsafe/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/unsafe/rwlock/rwlockreadguard_code.v
@@ -19,13 +19,13 @@ Section rwlockreadguard_functions.
       delete [ #1; "x"];; "return" ["r"].
 
   Lemma rwlockreadguard_deref_type ty :
-    typed_instruction_ty [] [] [] rwlockreadguard_deref
+    typed_val rwlockreadguard_deref
       (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
           (fun '(α, β) => [# &shr{α}(rwlockreadguard β ty)]%T)
           (fun '(α, β) => &shr{α}ty)%T).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([α β] ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
     iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -60,11 +60,11 @@ Section rwlockreadguard_functions.
          else "loop" []).
 
   Lemma rwlockreadguard_drop_type ty :
-    typed_instruction_ty [] [] [] rwlockreadguard_drop
-                         (fn(∀ α, [☀α]; rwlockreadguard α ty) → unit).
+    typed_val rwlockreadguard_drop
+                   (fn(∀ α, [☀α]; rwlockreadguard α ty) → unit).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|by apply read_own_move|done|].
       iIntros (x'). simpl_subst.
     iApply (type_cont [] [] (λ _, [x ◁ _; x' ◁ _])%TC);
diff --git a/theories/typing/unsafe/rwlock/rwlockwriteguard_code.v b/theories/typing/unsafe/rwlock/rwlockwriteguard_code.v
index fd7c64365217a11973a767a86185a39a4bdb00d1..b5a30a2855039d68745e1a0fff2588bb314000db 100644
--- a/theories/typing/unsafe/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/unsafe/rwlock/rwlockwriteguard_code.v
@@ -19,13 +19,13 @@ Section rwlockwriteguard_functions.
       delete [ #1; "x"];; "return" ["r"].
 
   Lemma rwlockwriteguard_deref_type ty :
-    typed_instruction_ty [] [] [] rwlockwriteguard_deref
+    typed_val rwlockwriteguard_deref
       (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
           (fun '(α, β) => [# &shr{α}(rwlockwriteguard β ty)]%T)
           (fun '(α, β) => &shr{α}ty)%T).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([α β] ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
     iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -61,13 +61,13 @@ Section rwlockwriteguard_functions.
       delete [ #1; "x"];; "return" ["r"].
 
   Lemma rwlockwriteguard_derefmut_type ty :
-    typed_instruction_ty [] [] [] rwlockwriteguard_derefmut
+    typed_val rwlockwriteguard_derefmut
       (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
           (fun '(α, β) => [# &uniq{α}(rwlockwriteguard β ty)]%T)
           (fun '(α, β) => &uniq{α}ty)%T).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([α β] ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
     iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -109,11 +109,11 @@ Section rwlockwriteguard_functions.
       let: "r" := new [ #0] in "return" ["r"].
 
   Lemma rwlockwriteguard_drop_type ty :
-    typed_instruction_ty [] [] [] rwlockwriteguard_drop
-                         (fn(∀ α, [☀α]; rwlockwriteguard α ty) → unit).
+    typed_val rwlockwriteguard_drop
+                   (fn(∀ α, [☀α]; rwlockwriteguard α ty) → unit).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
-      inv_vec arg=>x. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|by apply read_own_move|done|].
       iIntros (x'). simpl_subst.
     iIntros (tid qE) "#LFT Hna Hα HL Hk HT".
diff --git a/theories/typing/unsafe/spawn.v b/theories/typing/unsafe/spawn.v
index 83c50f58b413bb2e578a494d0304c9de7ecebe15..beb525a3650bbde44a0251a28bf281d3ae865bfb 100644
--- a/theories/typing/unsafe/spawn.v
+++ b/theories/typing/unsafe/spawn.v
@@ -68,11 +68,10 @@ Section spawn.
       delete [ #1; "f"];; "return" ["r"].
 
   Lemma spawn_type `(!Send envty, !Send retty) :
-    typed_instruction_ty [] [] [] spawn
-        (fn([]; fn([] ; envty) → retty, envty) → join_handle retty).
+    typed_val spawn (fn([]; fn([] ; envty) → retty, envty) → join_handle retty).
   Proof. (* FIXME: typed_instruction_ty is not used for printing. *)
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (_ ret arg).
-      inv_vec arg=>f env. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ret arg). inv_vec arg=>f env. simpl_subst.
     iApply type_deref; [solve_typing..|exact: read_own_move|done|].
     iIntros (f'). simpl_subst.
     iApply (type_let _ _ _ _ ([f' ◁ _; env ◁ _]%TC)
@@ -117,11 +116,10 @@ Section spawn.
       delete [ #1; "c"];; "return" ["r"].
 
   Lemma join_type retty :
-    typed_instruction_ty [] [] [] join
-        (fn([]; join_handle retty) → retty).
+    typed_val join (fn([]; join_handle retty) → retty).
   Proof.
-    iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (_ ret arg).
-      inv_vec arg=>c. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ret arg). inv_vec arg=>c. simpl_subst.
     iApply type_deref; [solve_typing..|exact: read_own_move|done|].
       iIntros (c'); simpl_subst.
     iApply (type_let _ _ _ _ ([c' ◁ _]%TC)