diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 0c0d96edc86b3123cd613ed419cf68c9759ba101..59a0474aadb20523bc1197e7dd2c05aed6476970 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -13,11 +13,8 @@ Section get_x.
 
   Lemma get_x_type :
     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.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
     inv_vec p=>p. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (p'); simpl_subst.
     iApply (type_letalloc_1 (&shr{α}int)); [solve_typing..|]. iIntros (r). simpl_subst.
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index b13fe440196806f1c38bfedbcf66829ee1d02589..77b4de9189d541f1890ffd314e21a4a723a865e3 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -14,7 +14,7 @@ Section init_prod.
 
   Lemma init_prod_type : typed_val init_prod (fn(∅; int, int) → Π[int;int]).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([] ϝ ret p). inv_vec p=>x y. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (y'). simpl_subst.
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 12d8c2956bdb76cb7b855ca3091aa544028a62cb..4d417260d5c054fd16620135916c3acec4372bb1 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -19,7 +19,7 @@ Section lazy_lft.
 
   Lemma lazy_lft_type : typed_val lazy_lft (fn(∅) → unit).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. 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 a434296c11933105dcd57600436714d10dee3752..1019fb9f4af41fc21c5bb7cc55eb807f0398c952 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -19,7 +19,7 @@ Section rebor.
   Lemma rebor_type :
     typed_val rebor (fn(∅; Π[int; int], Π[int; int]) → int).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. 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 586e2aa81acde2265196dfdbda8e103df23dead6..639017be47047c71a599d3457a4759e826bce028 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -14,7 +14,7 @@ Section unbox.
   Lemma ubox_type :
     typed_val unbox (fn(∀ α, ∅; &uniq{α}box (Π[int; int])) → &uniq{α} int).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret b). inv_vec b=>b. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (b'); simpl_subst.
     iApply type_deref_uniq_own; [solve_typing..|]. iIntros (bx); simpl_subst.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index eed357184829641af52f3b9c4cf0f980f0d55699..55183c084441e6af707216957917af0489a3b39e 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -120,7 +120,7 @@ Arguments fn_params {_ _} _.
    printing. Once on 8.6pl1, this should work.  *)
 Notation "'fn(∀' x .. x' ',' E ';' T1 ',' .. ',' TN ')' '→' R" :=
   (fn (λ x, (.. (λ x',
-      FP_wf E%EL (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T R%T)..)))
+      FP_wf E%EL (Vector.cons T1%T .. (Vector.cons TN%T Vector.nil) ..) R%T)..)))
   (at level 99, R at level 200, x binder, x' binder,
    format "'fn(∀'  x .. x' ','  E ';'  T1 ','  .. ','  TN ')'  '→'  R") : lrust_type_scope.
 Notation "'fn(∀' x .. x' ',' E ')' '→' R" :=
@@ -128,7 +128,7 @@ Notation "'fn(∀' x .. x' ',' E ')' '→' R" :=
   (at level 99, R at level 200, x binder, x' binder,
    format "'fn(∀'  x .. x' ','  E ')'  '→'  R") : lrust_type_scope.
 Notation "'fn(' E ';' T1 ',' .. ',' TN ')' '→' R" :=
-  (fn (λ _:(), FP_wf E%EL (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..) R%T))
+  (fn (λ _:(), FP_wf E%EL (Vector.cons T1%T .. (Vector.cons TN%T Vector.nil) ..) R%T))
   (at level 99, R at level 200,
    format "'fn(' E ';'  T1 ','  .. ','  TN ')'  '→'  R") : lrust_type_scope.
 Notation "'fn(' E ')' '→' R" :=
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index c3f87addea9454641d3d3a207b33c7510d513088..2220e79dd67e0a042e832fbfcb1996aaa264d4f4 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -32,7 +32,6 @@ Section lft_contexts.
 
   Definition elctx_interp (E : elctx) : iProp Σ :=
     ([∗ list] x ∈ E, elctx_elt_interp x)%I.
-  Global Arguments elctx_interp _%EL.
   Global Instance elctx_interp_permut :
     Proper ((≡ₚ) ==> (⊣⊢)) elctx_interp.
   Proof. intros ???. by apply big_opL_permutation. Qed.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index eff85844154f2370d2f2ea007e7da6c306f1b61f..023d116ba6ba3e7bd3099e97e026dcfd1938fb3f 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -90,7 +90,7 @@ Section typing.
 
   Lemma cell_new_type ty `{!TyWf ty} : typed_val cell_new (fn(∅; ty) → cell ty).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_jump; [solve_typing..|].
     iIntros (??) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
@@ -102,7 +102,7 @@ Section typing.
   Lemma cell_into_inner_type ty `{!TyWf ty} :
     typed_val cell_into_inner (fn(∅; cell ty) → ty).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_jump; [solve_typing..|].
     iIntros (??) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
@@ -114,7 +114,7 @@ Section typing.
   Lemma cell_get_mut_type ty `{!TyWf ty} :
     typed_val cell_get_mut (fn(∀ α, ∅; &uniq{α} (cell ty)) → &uniq{α} ty).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. 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 /=.
@@ -131,7 +131,7 @@ Section typing.
   Lemma cell_get_type ty `{!TyWf ty} `(!Copy ty) :
     typed_val (cell_get ty) (fn(∀ α, ∅; &shr{α} (cell ty)) → ty).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
     iApply type_letalloc_n; [solve_typing| |iIntros (r); simpl_subst].
@@ -151,7 +151,7 @@ Section typing.
   Lemma cell_replace_type ty `{!TyWf ty} :
     typed_val (cell_replace ty) (fn(∀ α, ∅; &shr{α} cell ty, ty) → ty).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>c x. simpl_subst.
     iApply type_deref; [solve_typing..|].
     iIntros (c'); simpl_subst.
diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
index a641cdb3185aed68917c039bb6efcba7a51d1fbb..768aabdd2a1787edb6c50fa44ea71bb0e2118474 100644
--- a/theories/typing/lib/fake_shared_box.v
+++ b/theories/typing/lib/fake_shared_box.v
@@ -11,9 +11,9 @@ Section fake_shared_box.
 
   Lemma fake_shared_box_type ty `{!TyWf ty} :
     typed_val fake_shared_box
-      (fn (fun '(α, β) => FP_wf ∅ [# &shr{α}(&shr{β} ty)] (&shr{α}box ty))).
+      (fn(∀ '(α, β), ∅; &shr{α} &shr{β} ty) → &shr{α} box ty).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk HT".
     rewrite tctx_interp_singleton tctx_hasty_val.
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index fa7910354d792e9838fc296eb50ce1c8ec83add0..62224b9b19b3904adc6b89af2beda7a6d1b9220f 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -26,7 +26,7 @@ Section option.
     typed_val
       option_as_mut (fn(∀ α, ∅; &uniq{α} (option τ)) → option (&uniq{α}τ)).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
       inv_vec p=>o. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (o'). simpl_subst.
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
@@ -56,7 +56,7 @@ Section option.
   Lemma option_unwrap_or_type Ï„ `{!TyWf Ï„} :
     typed_val (option_unwrap_or τ) (fn(∅; option τ, τ) → τ).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. 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/lib/rc.v b/theories/typing/lib/rc.v
index 19de11598a057c3e9dbccb860af54e2c6c82ba6e..b05eb1fc059462fe38d29926ceb567dfbc6c68e8 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -259,7 +259,7 @@ Section code.
   Lemma rc_new_type ty `{!TyWf ty} :
     typed_val (rc_new ty) (fn(∅; ty) → rc ty).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|]; iIntros (rcbox); simpl_subst.
     iApply type_new; [solve_typing..|]; iIntros (rc); simpl_subst.
@@ -298,7 +298,7 @@ Section code.
   Lemma rc_clone_type ty `{!TyWf ty} :
     typed_val rc_clone (fn(∀ α, ∅; &shr{α} rc ty) → rc ty).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|]; iIntros (rc2); simpl_subst.
     rewrite (Nat2Z.id 1). (* Having to do this is rather annoying... *) 
@@ -359,7 +359,7 @@ Section code.
   Lemma rc_deref_type ty `{!TyWf ty} :
     typed_val rc_deref (fn(∀ α, ∅; &shr{α} rc ty) → &shr{α} ty).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
     iApply type_new; [solve_typing..|]; iIntros (x); simpl_subst. rewrite (Nat2Z.id 1).
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
@@ -410,7 +410,7 @@ Section code.
     typed_val (rc_try_unwrap ty) (fn(∅; rc ty) → Σ[ ty; rc ty ]).
   Proof.
     (* TODO: There is a *lot* of duplication between this proof and the one for drop. *)
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
     iIntros (_ ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
     iApply type_new; [solve_typing..|]; iIntros (x); simpl_subst.
     rewrite (Nat2Z.id (Σ[ ty; rc ty ]).(ty_size)).
@@ -481,7 +481,7 @@ Section code.
   Lemma rc_drop_type ty `{!TyWf ty} :
     typed_val (rc_drop ty) (fn(∅; rc ty) → option ty).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
     iIntros (_ ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
     iApply type_new; [solve_typing..|]; iIntros (x); simpl_subst.
     rewrite (Nat2Z.id (option ty).(ty_size)).
@@ -556,7 +556,7 @@ Section code.
   Lemma rc_get_mut_type ty `{!TyWf ty} :
     typed_val rc_get_mut (fn(∀ α, ∅; &uniq{α} rc ty) → option (&uniq{α} ty)).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
     iApply type_new; [solve_typing..|]; iIntros (x); simpl_subst. rewrite (Nat2Z.id 2%nat).
     iApply (type_cont [] [ϝ ⊑ₗ []]
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 40ff2375a143fb6f3acccf786415db32ff63cae6..c1a28bb728b2b51b057babe45b5f6577f8ab1e36 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -58,7 +58,7 @@ Section ref_functions.
     typed_val ref_clone (fn (fun '(α, β) =>
                 FP_wf ∅ [# &shr{α}(ref β ty)]%T (ref β ty)%T)).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
     iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
@@ -120,7 +120,7 @@ Section ref_functions.
     typed_val ref_deref
       (fn (fun '(α, β) => FP_wf ∅ [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T)).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
     iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
@@ -156,7 +156,7 @@ Section ref_functions.
   Lemma ref_drop_type ty `{!TyWf ty} :
     typed_val ref_drop (fn(∀ α, ∅; ref α ty) → unit).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk Hx". rewrite tctx_interp_singleton tctx_hasty_val.
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
@@ -221,7 +221,7 @@ Section ref_functions.
       (fn(∀ β, ∅; ref β ty1, fn(∀ α, ∅; envty, &shr{α}ty1) → &shr{α}ty2, envty)
        → ref β ty2).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
        inv_vec arg=>ref f env. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (f'). simpl_subst.
     iApply (type_newlft [ϝ]). iIntros (κ tid) "#LFT #HE Hna HL Hk (Hf & #Hf' & Href & Henv)".
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index f633a56179dfebddebd1b5c4816cdae0dd18b4b1..fcea5370e14fb2cbd500e6cfa8f2a312e9659f2b 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -22,7 +22,7 @@ Section refcell_functions.
   Lemma refcell_new_type ty `{!TyWf ty} :
     typed_val (refcell_new ty) (fn(∅; ty) → refcell ty).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|].
     iIntros (r tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
@@ -57,7 +57,7 @@ Section refcell_functions.
   Lemma refcell_into_inner_type ty `{!TyWf ty} :
     typed_val (refcell_into_inner ty) (fn(∅; refcell ty) → ty).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|].
     iIntros (r tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
@@ -92,7 +92,7 @@ Section refcell_functions.
     typed_val refcell_get_mut
               (fn(∀ α, ∅; &uniq{α} (refcell ty)) → &uniq{α} ty)%T.
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL HC HT".
@@ -143,7 +143,7 @@ Section refcell_functions.
     typed_val refcell_try_borrow
       (fn(∀ α, ∅; &shr{α}(refcell ty)) → option (ref α ty)).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ box (&shr{α} refcell ty);
@@ -250,7 +250,7 @@ Section refcell_functions.
     typed_val refcell_try_borrow_mut
               (fn(∀ α, ∅; &shr{α}(refcell ty)) → option (refmut α ty))%T.
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ box (&shr{α} refcell ty);
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 3dd1961e2deff8941e9388c4f785a6c2314c1044..24b3e4e40b862a1829e0d0f08376e40ba1e6e189 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -22,7 +22,7 @@ Section refmut_functions.
     typed_val refmut_deref (fn (fun '(α, β) =>
        FP_wf ∅ [# &shr{α}(refmut β ty)]%T (&shr{α}ty))).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
     iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
@@ -65,7 +65,7 @@ Section refmut_functions.
     typed_val refmut_derefmut (fn (fun '(α, β) =>
       FP_wf ∅ [# &uniq{α}(refmut β ty)]%T (&uniq{α}ty)%T)).
    Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
     iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
@@ -118,7 +118,7 @@ Section refmut_functions.
   Lemma refmut_drop_type ty `{!TyWf ty} :
     typed_val refmut_drop (fn(∀ α, ∅; refmut α ty) → unit).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk Hx". rewrite tctx_interp_singleton tctx_hasty_val.
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
@@ -174,7 +174,7 @@ Section refmut_functions.
             fn(∀ α, ∅; envty, &uniq{α} ty1) → &uniq{α} ty2, envty)
        → refmut β ty2).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
        inv_vec arg=>ref f env. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (f'). simpl_subst.
     iApply (type_newlft [ϝ]). iIntros (κ tid) "#LFT #HE Hna HL Hk (Hf & #Hf' & Href & Henv)".
@@ -196,7 +196,7 @@ Section refmut_functions.
     iAssert (κ ⊑ α ⊓ ν)%I with "[>Hb]" as "#Hκν".
     { iApply (lft_incl_glb with "Hκα"). iApply (frac_bor_lft_incl with "LFT").
       iApply (bor_fracture with "LFT [> -]"); first done. rewrite /= Qp_mult_1_r //. }
-    iApply (type_type ((κ ⊑ₑ α ⊓ ν) :: (α ⊓ ν ⊑ₑ α) :: _)%EL _
+    iApply (type_type ((κ ⊑ₑ α ⊓ ν) :: (α ⊓ ν ⊑ₑ α) :: _) _
         [k ◁cont(_, λ x:vec val 1, [ x!!!0 ◁ box (&uniq{α ⊓ ν}ty2)])]
         [ f' ◁ fn(∀ α, ∅; envty, &uniq{α}ty1) → &uniq{α}ty2;
           #lx ◁ box (&uniq{α ⊓ ν}ty1); env ◁ box envty ]
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 8b48334ef5e30cb4e0302c9e934b74c312fc87aa..a82f950b028c05a9d1e79389cd42cefde77d92ec 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -22,7 +22,7 @@ Section rwlock_functions.
   Lemma rwlock_new_type ty `{!TyWf ty} :
     typed_val (rwlock_new ty) (fn(∅; ty) → rwlock ty).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ret ϝ arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|].
     iIntros (r tid) "#LFT HE Hna HL Hk HT". simpl_subst.
@@ -58,7 +58,7 @@ Section rwlock_functions.
   Lemma rwlock_into_inner_type ty `{!TyWf ty} :
     typed_val (rwlock_into_inner ty) (fn(∅; rwlock ty) → ty).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ret ϝ arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|].
     iIntros (r tid) "#LFT HE Hna HL Hk HT". simpl_subst.
@@ -92,7 +92,7 @@ Section rwlock_functions.
   Lemma rwlock_get_mut_type ty `{!TyWf ty} :
     typed_val rwlock_get_mut (fn(∀ α, ∅; &uniq{α} (rwlock ty)) → &uniq{α} ty).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
     iIntros (tid) "#LFT HE Hna HL HC HT".
@@ -143,7 +143,7 @@ Section rwlock_functions.
     typed_val rwlock_try_read
         (fn(∀ α, ∅; &shr{α}(rwlock ty)) → option (rwlockreadguard α ty)).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
@@ -258,7 +258,7 @@ Section rwlock_functions.
     typed_val rwlock_try_write
         (fn(∀ α, ∅; &shr{α}(rwlock ty)) → option (rwlockwriteguard α ty)).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. 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))]));
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 83a178eca85201599fd3addd989a8a576a375848..a7b8630ed089d617243c536d50ade4d91555d8b4 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -20,9 +20,9 @@ Section rwlockreadguard_functions.
 
   Lemma rwlockreadguard_deref_type ty `{!TyWf ty} :
     typed_val rwlockreadguard_deref
-      (fn (fun '(α, β) => FP_wf ∅ [# &shr{α}(rwlockreadguard β ty)] (&shr{α}ty))).
+      (fn(∀ '(α, β), ∅; &shr{α} rwlockreadguard β ty) → &shr{α} ty).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
     iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
@@ -61,7 +61,7 @@ Section rwlockreadguard_functions.
   Lemma rwlockreadguard_drop_type ty `{!TyWf ty} :
     typed_val rwlockreadguard_drop (fn(∀ α, ∅; rwlockreadguard α ty) → unit).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
     iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ _; x' ◁ _]));
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index a31256ba50b4292f7b6c7e26ef1f075a168cdfaf..234c671e3d7136eff0984856efb2d29d2581d456 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -20,9 +20,9 @@ Section rwlockwriteguard_functions.
 
   Lemma rwlockwriteguard_deref_type ty `{!TyWf ty} :
     typed_val rwlockwriteguard_deref
-      (fn (fun '(α, β) => FP_wf ∅ [# &shr{α}(rwlockwriteguard β ty)] (&shr{α}ty))).
+      (fn(∀ '(α, β), ∅; &shr{α} rwlockwriteguard β ty) → &shr{α} ty).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
     iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
@@ -64,9 +64,9 @@ Section rwlockwriteguard_functions.
 
   Lemma rwlockwriteguard_derefmut_type ty `{!TyWf ty} :
     typed_val rwlockwriteguard_derefmut
-      (fn (fun '(α, β) => FP_wf ∅ [# &uniq{α}(rwlockwriteguard β ty)] (&uniq{α}ty))).
+      (fn(∀ '(α, β), ∅; &uniq{α} rwlockwriteguard β ty) → &uniq{α} ty).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
     iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
@@ -111,7 +111,7 @@ Section rwlockwriteguard_functions.
     typed_val rwlockwriteguard_drop
               (fn(∀ α, ∅; rwlockwriteguard α ty) → unit).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk HT".
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index d4b5bc8dc4996ccef66e07e48cefa4af403d90a9..8f2715c72ff4ce71959582900109e4e1d18a9770 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -73,9 +73,9 @@ Section spawn.
   Lemma spawn_type envty retty `{!TyWf envty, !TyWf retty}
         `(!Send envty, !Send retty) :
     let E ϝ := envty.(ty_outlives_E) static ++ retty.(ty_outlives_E) static in
-    typed_val spawn (fn(E; fn(∅; envty) → retty, envty) → join_handle retty).
-  Proof. (* FIXME: typed_instruction_ty is not used for printing. *)
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    typed_val spawn (fn(E; (fn(∅; envty) → retty), envty) → join_handle retty).
+  Proof.
+    intros ? E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>f env. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (f'). simpl_subst.
     iApply (type_let _ _ _ _ ([f' ◁ _; env ◁ _])
@@ -120,7 +120,7 @@ Section spawn.
   Lemma join_type retty `{!TyWf retty} :
     typed_val join (fn(∅; join_handle retty) → retty).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>c. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (c'); simpl_subst.
     iApply (type_let _ _ _ _ ([c' ◁ _])
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index c88f822eccff224649f7a66c1933cafeb5394178..c25b5a529e082ff0664041ba9a907821d68b8faf 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -78,10 +78,14 @@ Section typing.
   Global Arguments typed_read _ _ _%T _%T _%T.
 End typing.
 
-Notation typed_instruction_ty E L T e ty :=
-  (typed_instruction E L T e (λ v : val, [v ◁ ty%list%T])).
+Definition typed_instruction_ty `{typeG Σ} (E : elctx) (L : llctx) (T : tctx)
+    (e : expr) (ty : type) : iProp Σ :=
+  typed_instruction E L T e (λ v, [v ◁ ty]).
+Arguments typed_instruction_ty {_ _} _ _ _ _%E _%T.
 
-Notation typed_val v ty := (∀ E L, typed_instruction_ty E L [] (of_val v) ty).
+Definition typed_val `{typeG Σ} (v : val) (ty : type) : Prop :=
+  ∀ E L, typed_instruction_ty E L [] (of_val v) ty.
+Arguments typed_val _ _ _%V _%T.
 
 Section typing_rules.
   Context `{typeG Σ}.