diff --git a/_CoqProject b/_CoqProject
index daf46408eff9239ceaf5292994843b402e13f42f..dc849794fb19e072d34f46b76921bfbc09110955 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -38,3 +38,4 @@ theories/typing/product_split.v
 theories/typing/type_sum.v
 theories/typing/fixpoint.v
 theories/typing/cont.v
+theories/typing/function.v
diff --git a/theories/lang/memcpy.v b/theories/lang/memcpy.v
index ab2ce857e1591bae0243f3d927986d4d88e6b408..f4aa87e89e418ca9e2f82a20774e5ca5626b9fe0 100644
--- a/theories/lang/memcpy.v
+++ b/theories/lang/memcpy.v
@@ -19,11 +19,11 @@ Notation "e1 <-{ n ',Σ' i } ! e2" :=
   (at level 80, n, i at next level,
    format "e1  <-{ n ,Σ  i }  ! e2") : expr_scope.
 
-Lemma wp_memcpy `{noprolG Σ} E l1 l2 vl1 vl2 q (n : Z):
+Lemma wp_memcpy `{noprolG Σ} tid E l1 l2 vl1 vl2 q (n : Z):
   Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
-  {{{ ⎡l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2⎤ }}}
-    #l1 <-{n} !#l2 @ E
-  {{{ RET #☠; ⎡l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2⎤ }}}.
+  {{{ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
+    #l1 <-{n} !#l2 in tid @ E
+  {{{ RET #☠; l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2 }}}.
 Proof.
   iIntros (Hvl1 Hvl2 Φ) "(Hl1 & Hl2) HΦ".
   iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op; case_bool_decide; wp_if.
diff --git a/theories/lang/new_delete.v b/theories/lang/new_delete.v
index b3353d74ebcc126ecafceb568cf5c7a03076c85c..759d68006fbf23317db61ff5165c735d4b4c07bb 100644
--- a/theories/lang/new_delete.v
+++ b/theories/lang/new_delete.v
@@ -16,11 +16,11 @@ Definition delete : val :=
 Section specs.
   Context `{noprolG Σ}.
 
-  Lemma wp_new E (n : Z):
+  Lemma wp_new E tid (n : Z):
     (0 ≤ n)%Z →
-    {{{ True }}} new [ #n ] @ E
+    {{{ True }}} new [ #n ] in tid @ E
     {{{ l, RET LitV $ LitLoc l;
-        (⎡†l…(Z.to_nat n)⎤ ∨ ⌜n = 0⌝) ∗ ⎡l ↦∗ repeat AVal (Z.to_nat n)⎤ }}}.
+        (⎡†l…(Z.to_nat n)⎤ ∨ ⌜n = 0⌝) ∗ l ↦∗ repeat AVal (Z.to_nat n) }}}.
   Proof.
     iIntros (? Φ) "_ HΦ". wp_lam. wp_op; case_bool_decide.
     - wp_if. assert (n = 0) as -> by lia. iApply "HΦ".
@@ -28,10 +28,10 @@ Section specs.
     - wp_if. wp_alloc l as "H↦" "H†". omega. iApply "HΦ". subst sz. iFrame.
   Qed.
 
-  Lemma wp_delete E (n:Z) l vl :
+  Lemma wp_delete E tid (n:Z) l vl :
     n = length vl →
-    {{{ ⎡l ↦∗ vl⎤ ∗ (⎡†l…(length vl)⎤ ∨ ⌜n = 0⌝) }}}
-      delete [ #n; #l] @ E
+    {{{ l ↦∗ vl ∗ (⎡†l…(length vl)⎤ ∨ ⌜n = 0⌝) }}}
+      delete [ #n; #l] in tid @ E
     {{{ RET #☠; True }}}.
   Proof.
     iIntros (? Φ) "[H↦ [H†|%]] HΦ";
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 74433575c1f2884bf065e6266976dac31f3460d6..db989c9263277ffad94056b8f6e9246c93dded1d 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -41,9 +41,7 @@ Section typing.
     typed_body E L C T (if: p then e1 else e2).
   Proof.
     iIntros (Hp) "He1 He2". iIntros (tid) "#LFT #HE Htl HL HC HT".
-    rewrite !(embed_big_sepL _ T).
     iDestruct (bi.big_sepL_elem_of _ _ _ Hp with "HT") as "#Hp".
-    rewrite -!(embed_big_sepL _ T).
     wp_bind p. iApply (wp_hasty with "Hp").
     iIntros ([[| |[|[]|]]|]) "_ /="; iIntros ([]); [|]; wp_case.
     - iApply ("He2" with "LFT HE Htl HL HC HT").
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index a81a65299c1ce9b9d51c920f4fd903f0a42e81ba..cc86cd555c2d1615aca7ae279b1a1af31dbd0767 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -100,7 +100,7 @@ Section borrow.
       iMod (bor_sep with "[LFT //] Hbor") as "[_ Hbor]". done.
       iMod ("Hclose" with "Htok") as "($ & $)".
       by rewrite tctx_interp_singleton tctx_hasty_val' //=.
-    - iIntros "!> !> (?&?&?) !>". iNext. iExists _.
+    - iIntros "!> (?&?&?) !>". iNext. iExists _.
       rewrite -own_loc_na_vec_singleton. iFrame. by iFrame.
     - iFrame.
   Qed.
@@ -123,7 +123,7 @@ Section borrow.
     wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try iDestruct "Hown" as %[].
     iDestruct "Hown" as (l') "#[H↦b #Hown]".
     iMod (frac_bor_acc with "[LFT //] H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
-    iApply (wp_step_fupd _ (_∖_) with "[Hown Htok2]"); try done.
+    iApply (wp_step_fupd _ _ (_∖_) with "[Hown Htok2]"); try done.
     - iMod ("Hown" with "[%] Htok2") as "H"; first solve_ndisj. iModIntro.
       iNext. iMod "H". iApply "H".
     - iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
@@ -182,10 +182,10 @@ Section borrow.
     wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hshr"; try by iDestruct "Hshr" as %[].
     iDestruct "Hshr" as (l') "[H↦ Hown]".
     iMod (frac_bor_acc with "[LFT //] H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
-    iAssert ⎡κ ⊑ κ' ⊓ κ⎤%I as "#Hincl'".
+    iAssert (κ ⊑ κ' ⊓ κ)%I as "#Hincl'".
     { iApply (lft_incl_glb with "Hincl []"). iApply lft_incl_refl. }
     iMod (lft_incl_acc with "Hincl' Htok2") as (q2) "[Htok2 Hclose'']"; first solve_ndisj.
-    iApply (wp_step_fupd _ (_∖_) with "[Hown Htok2]"); try done.
+    iApply (wp_step_fupd _ _ (_∖_) with "[Hown Htok2]"); try done.
     - iMod ("Hown" with "[%] Htok2") as "Hown"; first solve_ndisj. iModIntro. iNext.
       iMod "Hown". iApply "Hown".
     - iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index 5875a3449ea542658d5f151dd1ee41cc1c454e99..25b906d8e57902519b69837d9773ea40b24be7ac 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 Section cont_context_def.
   Context `{typeG Σ}.
 
-  Definition cont_postcondition : tvProp Σ := True%I.
+  Definition cont_postcondition : vProp Σ := True%I.
 
   Record cctx_elt : Type :=
     CCtx_iscont { cctxe_k : val; cctxe_L : llctx;
@@ -21,11 +21,13 @@ Notation "k ◁cont( L , T )" := (CCtx_iscont k L _ T)
 Section cont_context.
   Context `{typeG Σ}.
 
-  Definition cctx_elt_interp (tid : thread_id) (x : cctx_elt) : tvProp Σ :=
+  Definition cctx_elt_interp (tid : thread_id) (x : cctx_elt) : vProp Σ :=
     let '(k ◁cont(L, T)) := x in
-    (∀ args, ⎡na_own tid top⎤ -∗ ⎡llctx_interp L 1⎤ -∗ ⎡tctx_interp tid (T args)⎤ -∗
-         WP k (base.of_val <$> (args : list _)) {{ _, cont_postcondition }})%I.
-  Definition cctx_interp (tid : thread_id) (C : cctx) : tvProp Σ :=
+    (∀ args, na_own tid.(tid_na_inv_pool) top -∗
+         llctx_interp L 1 -∗ tctx_interp tid (T args) -∗
+         WP k (base.of_val <$> (args : list _)) in tid.(tid_tid)
+           {{ _, cont_postcondition }})%I.
+  Definition cctx_interp (tid : thread_id) (C : cctx) : vProp Σ :=
     (∀ (x : cctx_elt), ⌜x ∈ C⌝ -∗ cctx_elt_interp tid x)%I.
 
   Global Instance cctx_interp_permut tid:
@@ -65,7 +67,7 @@ Section cont_context.
   Qed.
 
   Definition cctx_incl (E : elctx) (C1 C2 : cctx): Prop :=
-    ∀ tid, ⎡lft_ctx⎤ -∗ ⎡elctx_interp E⎤ -∗
+    ∀ tid, ⎡lft_ctx⎤ -∗ elctx_interp E -∗
             cctx_interp tid C1 -∗ cctx_interp tid C2.
 
   Global Instance cctx_incl_preorder E : PreOrder (cctx_incl E).
diff --git a/theories/typing/function.v b/theories/typing/function.v
new file mode 100644
index 0000000000000000000000000000000000000000..eb81024a97bdec4946d2f8975490cca97cdbf3f3
--- /dev/null
+++ b/theories/typing/function.v
@@ -0,0 +1,433 @@
+From iris.algebra Require Import vector list.
+From lrust.typing Require Export type.
+From lrust.typing Require Import own programs cont.
+Set Default Proof Using "Type".
+
+Section fn.
+  Context `{typeG Σ} {A : Type} {n : nat}.
+
+  Record fn_params := FP { fp_E : lft → elctx; fp_tys : vec type n; fp_ty : type }.
+
+  Definition FP_wf E (tys : vec type n) `{!TyWfLst tys} ty `{!TyWf ty} :=
+    FP (λ ϝ, E ϝ ++ tys.(tyl_wf_E) ++ tys.(tyl_outlives_E) ϝ ++
+                    ty.(ty_wf_E) ++ ty.(ty_outlives_E) ϝ)
+       tys ty.
+
+  (* The other alternative for defining the fn type would be to state
+     that the value applied to its parameters is a typed body whose type
+     is the return type.
+     That would be slightly simpler, but, unfortunately, we are no longer
+     able to prove that this is contractive. *)
+  Program Definition fn (fp : A → fn_params) : type :=
+    {| st_own tid vl := tc_opaque (∃ fb kb xb e H,
+         ⌜vl = [VVal $ @RecV fb (kb::xb) e H]⌝ ∗ ⌜length xb = n⌝ ∗
+         ▷ ∀ (x : A) (ϝ : lft) (k : val) (xl : vec val (length xb)),
+            □ (typed_body ((fp x).(fp_E)  ϝ) [ϝ ⊑ₗ []]
+                         [k◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
+                         (zip_with (TCtx_hasty ∘ of_val) xl
+                                   (box <$> (vec_to_list (fp x).(fp_tys))))
+                         (subst_v (fb::kb::xb) (RecV fb (kb::xb) e:::k:::xl) e)))%I |}.
+  Next Obligation.
+    iIntros (fp tid vl)  "H". iDestruct "H" as (fb kb xb e ?) "[% _]". by subst.
+  Qed.
+  Next Obligation. simpl. apply _. Qed.
+
+  (* FIXME : This definition is less restrictive than the one used in
+     Rust. In Rust, the type of parameters are taken into account for
+     well-formedness, and all the liftime constrains relating a
+     generalized liftime are ignored. For simplicity, we ignore all of
+     them, but this is not very faithful. *)
+  Global Instance fn_wf fp : TyWf (fn fp) :=
+    { ty_lfts := []; ty_wf_E := [] }.
+
+  Global Instance fn_send fp : Send (fn fp).
+  Proof. iIntros (tid1 tid2 vl). done. Qed.
+
+  Definition fn_params_rel (ty_rel : relation type) : relation fn_params :=
+    λ fp1 fp2,
+      Forall2 ty_rel fp2.(fp_tys) fp1.(fp_tys) ∧ ty_rel fp1.(fp_ty) fp2.(fp_ty) ∧
+      pointwise_relation lft eq fp1.(fp_E) fp2.(fp_E).
+
+  Global Instance fp_tys_proper R :
+    Proper (flip (fn_params_rel R) ==> (Forall2 R : relation (vec _ _))) fp_tys.
+  Proof. intros ?? HR. apply HR. Qed.
+  Global Instance fp_tys_proper_flip R :
+    Proper (fn_params_rel R ==> flip (Forall2 R : relation (vec _ _))) fp_tys.
+  Proof. intros ?? HR. apply HR. Qed.
+
+  Global Instance fp_ty_proper R :
+    Proper (fn_params_rel R ==> R) fp_ty.
+  Proof. intros ?? HR. apply HR. Qed.
+
+  Global Instance fp_E_proper R :
+    Proper (fn_params_rel R ==> eq ==> eq) fp_E.
+  Proof. intros ?? HR ??->. apply HR. Qed.
+
+  Global Instance FP_proper R :
+    Proper (pointwise_relation lft eq ==>
+            flip (Forall2 R : relation (vec _ _)) ==> R ==>
+            fn_params_rel R) FP.
+  Proof. by split; [|split]. Qed.
+
+  Global Instance fn_type_contractive n' :
+    Proper (pointwise_relation A (fn_params_rel (type_dist2_later n')) ==>
+            type_dist2 n') fn.
+  Proof.
+    intros fp1 fp2 Hfp. apply ty_of_st_type_ne. destruct n'; first done.
+    constructor; unfold ty_own; simpl.
+    (* TODO: 'f_equiv' is slow here because reflexivity is slow. *)
+    (* The clean way to do this would be to have a metric on type contexts. Oh well. *)
+    intros tid vl. unfold typed_body.
+    do 12 f_equiv. f_contractive.
+    do 16 ((eapply fp_E_proper; try reflexivity) || exact: Hfp || f_equiv).
+    - rewrite !cctx_interp_singleton /=. do 5 f_equiv.
+      rewrite !tctx_interp_singleton /tctx_elt_interp /=.
+      do 5 f_equiv. apply type_dist2_dist. apply Hfp.
+    - rewrite /tctx_interp !bi.big_sepL_zip_with /=. do 4 f_equiv.
+      cut (∀ n tid p i, Proper (dist n ==> dist n)
+        (λ (l : list type),
+            match l !! i with
+            | Some ty => tctx_elt_interp tid (p ◁ ty) | None => emp
+            end)%I).
+      { intros Hprop. apply Hprop, list_fmap_ne; last first.
+        - symmetry. eapply Forall2_impl; first apply Hfp. intros.
+          apply dist_later_dist, type_dist2_dist_later. done.
+        - apply _. }
+      clear. intros n tid p i x y. rewrite list_dist_lookup=>/(_ i).
+      case _ : (x !! i)=>[tyx|]; case  _ : (y !! i)=>[tyy|];
+        inversion_clear 1; [solve_proper|done].
+  Qed.
+
+  Global Instance fn_ne n' :
+    Proper (pointwise_relation A (fn_params_rel (dist n')) ==> dist n') fn.
+  Proof.
+    intros ?? Hfp. apply dist_later_dist, type_dist2_dist_later.
+    apply fn_type_contractive=>u. split; last split.
+    - eapply Forall2_impl; first apply Hfp. intros. simpl.
+      apply type_dist_dist2. done.
+    - apply type_dist_dist2. apply Hfp.
+    - apply Hfp.
+  Qed.
+End fn.
+
+Arguments fn_params {_ _} _.
+
+(* We use recursive notation for binders as well, to allow patterns
+   like '(a, b) to be used. In practice, only one binder is ever used,
+   but using recursive binders is the only way to make Coq accept
+   patterns. *)
+(* FIXME : because of a bug in Coq, such patterns only work for
+   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%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" :=
+  (fn (λ x, (.. (λ x', FP_wf E%EL Vector.nil R%T)..)))
+  (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%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" :=
+  (fn (λ _:(), FP_wf E%EL Vector.nil R%T))
+  (at level 99, R at level 200,
+   format "'fn(' E ')'  '→'  R") : lrust_type_scope.
+
+Instance elctx_empty : Empty (lft → elctx) := λ ϝ, [].
+
+Section typing.
+  Context `{typeG Σ}.
+
+  Lemma fn_subtype {A n} E0 L0 (fp fp' : A → fn_params n) :
+    (∀ x ϝ, let EE := E0 ++ (fp' x).(fp_E) ϝ in
+            elctx_sat EE L0 ((fp x).(fp_E) ϝ) ∧
+            Forall2 (subtype EE L0) (fp' x).(fp_tys) (fp x).(fp_tys) ∧
+            subtype EE L0 (fp x).(fp_ty) (fp' x).(fp_ty)) →
+    subtype E0 L0 (fn fp) (fn fp').
+  Proof.
+    intros Hcons. apply subtype_simple_type=>//= qL. iIntros "HL0".
+    (* We massage things so that we can throw away HL0 before going under the box. *)
+    iAssert (∀ x ϝ, let EE := E0 ++ (fp' x).(fp_E) ϝ in □ (elctx_interp EE -∗
+                 elctx_interp ((fp x).(fp_E) ϝ) ∗
+                 ([∗ list] tys ∈ (zip (fp' x).(fp_tys) (fp x).(fp_tys)), type_incl (tys.1) (tys.2)) ∗
+                 type_incl (fp x).(fp_ty) (fp' x).(fp_ty)))%I as "#Hcons".
+    { iIntros (x ϝ). destruct (Hcons x ϝ) as (HE &Htys &Hty). clear Hcons.
+      iDestruct (HE with "HL0") as "#HE".
+      iDestruct (subtype_Forall2_llctx with "HL0") as "#Htys"; first done.
+      iDestruct (Hty with "HL0") as "#Hty".
+      iClear "∗". iIntros "!# #HEE".
+      iSplit; last iSplit.
+      - by iApply "HE".
+      - by iApply "Htys".
+      - by iApply "Hty". }
+    iClear "∗". clear Hcons. iIntros "!# #HE0 * Hf".
+    iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
+    iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. iNext.
+    rewrite /typed_body. iIntros (x ϝ k xl) "!# * #LFT #HE' Htl HL HC HT".
+    iDestruct ("Hcons" with "[$]") as "#(HE & Htys & Hty)".
+    iApply ("Hf" with "LFT HE Htl HL [HC] [HT]").
+    - unfold cctx_interp. iIntros (elt) "Helt".
+      iDestruct "Helt" as %->%elem_of_list_singleton. iIntros (ret) "Htl HL HT".
+      unfold cctx_elt_interp.
+      iApply ("HC" $! (_ ◁cont(_, _)) with "[%] Htl HL [> -]").
+      { by apply elem_of_list_singleton. }
+      rewrite /tctx_interp !bi.big_sepL_singleton /=.
+      iDestruct "HT" as (v) "[HP Hown]". iExists v. iFrame "HP".
+      iDestruct (box_type_incl with "[$Hty]") as "(_ & #Hincl & _)".
+      by iApply "Hincl".
+    - iClear "Hf". rewrite /tctx_interp
+         -{2}(fst_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length //
+         -{2}(snd_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length //
+         !zip_with_fmap_r !(zip_with_zip (λ _ _, (_ ∘ _) _ _)) !bi.big_sepL_fmap.
+      iApply (bi.big_sepL_impl with "HT"). iIntros "!#".
+      iIntros (i [p [ty1' ty2']]) "#Hzip H /=".
+      iDestruct "H" as (v) "[? Hown]". iExists v. iFrame.
+      rewrite !lookup_zip_with.
+      iDestruct "Hzip" as %(? & ? & ([? ?] & (? & Hty'1 &
+        (? & Hty'2 & [=->->])%bind_Some)%bind_Some & [=->->->])%bind_Some)%bind_Some.
+      iDestruct (bi.big_sepL_lookup with "Htys") as "#Hty'".
+      { rewrite lookup_zip_with /=. erewrite Hty'2. simpl. by erewrite Hty'1. }
+      iDestruct (box_type_incl with "[$Hty']") as "(_ & #Hincl & _)".
+      by iApply "Hincl".
+  Qed.
+
+  (* This proper and the next can probably not be inferred, but oh well. *)
+  Global Instance fn_subtype' {A n} E0 L0 :
+    Proper (pointwise_relation A (fn_params_rel (n:=n) (subtype E0 L0)) ==>
+            subtype E0 L0) fn.
+  Proof.
+    intros fp1 fp2 Hfp. apply fn_subtype=>x ϝ. destruct (Hfp x) as (Htys & Hty & HE).
+    split; last split.
+    - rewrite (HE ϝ). solve_typing.
+    - eapply Forall2_impl; first eapply Htys. intros ??.
+      eapply subtype_weaken; last done. by apply submseteq_inserts_r.
+    - eapply subtype_weaken, Hty; last done. by apply submseteq_inserts_r.
+  Qed.
+
+  Global Instance fn_eqtype' {A n} E0 L0 :
+    Proper (pointwise_relation A (fn_params_rel (n:=n) (eqtype E0 L0)) ==>
+            eqtype E0 L0) fn.
+  Proof.
+    intros fp1 fp2 Hfp. split; eapply fn_subtype=>x ϝ; destruct (Hfp x) as (Htys & Hty & HE); (split; last split).
+    - rewrite (HE ϝ). solve_typing.
+    - eapply Forall2_impl; first eapply Htys. intros t1 t2 Ht.
+      eapply subtype_weaken; last apply Ht; last done. by apply submseteq_inserts_r.
+    - eapply subtype_weaken; last apply Hty; last done. by apply submseteq_inserts_r.
+    - rewrite (HE ϝ). solve_typing.
+    - symmetry in Htys. eapply Forall2_impl; first eapply Htys. intros t1 t2 Ht.
+      eapply subtype_weaken; last apply Ht; last done. by apply submseteq_inserts_r.
+    - eapply subtype_weaken; last apply Hty; last done. by apply submseteq_inserts_r.
+  Qed.
+
+  Lemma fn_subtype_specialize {A B n} (σ : A → B) E0 L0 fp :
+    subtype E0 L0 (fn (n:=n) fp) (fn (fp ∘ σ)).
+  Proof.
+    apply subtype_simple_type=>//= qL.
+    iIntros "_ !# _ * Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
+    iExists fb, kb, xb, e, _. iSplit. done. iSplit. done.
+    rewrite /typed_body. iNext. iIntros "*". iApply "Hf".
+  Qed.
+
+  (* In principle, proving this hard-coded to an empty L would be sufficient --
+     but then we would have to require elctx_sat as an Iris assumption. *)
+  Lemma type_call_iris' E L (κs : list lft) {A} x (ps : list path) qκs qL tid
+        p (k : expr) (fp : A → fn_params (length ps)) :
+    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) L ((fp x).(fp_E) ϝ)) →
+    AsVal k →
+    ⎡lft_ctx⎤ -∗ elctx_interp E -∗ na_own tid.(tid_na_inv_pool) ⊤ -∗ llctx_interp L qL -∗
+    qκs.[lft_intersect_list κs] -∗
+    tctx_elt_interp tid (p ◁ fn fp) -∗
+    ([∗ list] y ∈ zip_with TCtx_hasty ps (box <$> vec_to_list (fp x).(fp_tys)),
+                   tctx_elt_interp tid y) -∗
+    (∀ ret, na_own tid.(tid_na_inv_pool) top -∗ llctx_interp L qL -∗
+             qκs.[lft_intersect_list κs] -∗
+             (box (fp x).(fp_ty)).(ty_own) tid [VVal ret] -∗
+             WP k [of_val ret] in tid.(tid_tid) {{ _, cont_postcondition }}) -∗
+    WP (call: p ps → k) in tid.(tid_tid) {{ _, cont_postcondition }}.
+  Proof.
+    iIntros (HE [k' Hk']) "#LFT #HE Htl HL Hκs Hf Hargs Hk". rewrite -(of_to_val k k') //.
+    clear dependent k. wp_apply (wp_hasty with "Hf"). iIntros (v) "% Hf".
+    iApply (wp_app_vec _ _ _ (_::_) ((λ v, ⌜v = (λ: ["_r"], (#☠ ;; #☠) ;; k' ["_r"])%V⌝):::
+               vmap (λ ty (v : val), tctx_elt_interp tid (v ◁ box ty)) (fp x).(fp_tys))%I
+            with "[Hargs]").
+    - rewrite /=. iSplitR "Hargs".
+      { simpl. iApply wp_value. by unlock. }
+      remember (fp_tys (fp x)) as tys. clear dependent k' p HE fp x.
+      iInduction ps as [|p ps] "IH" forall (tys); first by simpl.
+      simpl in tys. inv_vec tys=>ty tys. simpl.
+      iDestruct "Hargs" as "[HT Hargs]". iSplitL "HT".
+      + iApply (wp_hasty with "HT"). iIntros (?). rewrite tctx_hasty_val. iIntros "? $".
+      + iApply "IH". done.
+    - simpl. change (@length expr ps) with (length ps).
+      iIntros (vl'). inv_vec vl'=>kv vl; csimpl.
+      iIntros "[-> Hvl]". iDestruct "Hf" as (fb kb xb e ?) "[EQ [EQl #Hf]]".
+      iDestruct "EQ" as %[=->]. iDestruct "EQl" as %EQl.
+      revert vl fp HE. rewrite /= -EQl=>vl fp HE. wp_rec.
+      iMod (lft_create with "LFT") as (ϝ) "[Htk #Hinh]"; first done.
+      iSpecialize ("Hf" $! x ϝ _ vl). iDestruct (HE ϝ with "HL") as "#HE'".
+      iMod (bor_create _ ϝ with "LFT Hκs") as "[Hκs HκsI]"; first done.
+      iDestruct (frac_bor_lft_incl with "LFT [>Hκs]") as "#Hκs".
+      { iApply (bor_fracture with "LFT Hκs"); [|done].
+        split; [by rewrite Qp_mult_1_r|]. apply _. }
+      iApply ("Hf" with "LFT [] Htl [Htk] [Hk HκsI HL]").
+      + iApply "HE'". iIntros "{$# Hf Hinh HE' LFT HE %}".
+        iInduction κs as [|κ κs] "IH"=> //=. iSplitL.
+        { iApply lft_incl_trans; first done. iApply lft_intersect_incl_l. }
+        iApply "IH". iAlways. iApply lft_incl_trans; first done.
+        iApply lft_intersect_incl_r.
+      + iSplitL; last done. iExists ϝ. iSplit; first by rewrite /= left_id.
+        iFrame "#∗".
+      + iIntros (y) "IN". iDestruct "IN" as %->%elem_of_list_singleton.
+        iIntros (args) "Htl [Hϝ _] [Hret _]". inv_vec args=>r.
+        iDestruct "Hϝ" as  (κ') "(EQ & Htk & _)". iDestruct "EQ" as %EQ.
+        rewrite /= left_id in EQ. subst κ'. simpl. wp_rec. wp_bind Endlft.
+        iSpecialize ("Hinh" with "Htk"). iClear "Hκs".
+        iApply (wp_mask_mono _ (↑lftN)); first done.
+        iApply (wp_step_fupd with "Hinh"); [solve_ndisj..|]. wp_seq.
+        iIntros "#Htok !>". wp_seq. iMod ("HκsI" with "Htok") as ">Hκs".
+        iApply ("Hk" with "Htl HL Hκs"). rewrite tctx_hasty_val. done.
+      + rewrite /tctx_interp vec_to_list_map !zip_with_fmap_r
+                (zip_with_zip (λ v ty, (v, _))) zip_with_zip !bi.big_sepL_fmap.
+        iApply (bi.big_sepL_mono' with "Hvl"); last done. by iIntros (i [v ty']).
+  Qed.
+
+  Lemma type_call_iris E (κs : list lft) {A} x (ps : list path) qκs tid
+        f (k : expr) (fp : A → fn_params (length ps)) :
+    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) [] ((fp x).(fp_E) ϝ)) →
+    AsVal k →
+    ⎡lft_ctx⎤ -∗ elctx_interp E -∗ na_own tid.(tid_na_inv_pool) ⊤ -∗
+    qκs.[lft_intersect_list κs] -∗
+    (fn fp).(ty_own) tid [VVal f] -∗
+    ([∗ list] y ∈ zip_with TCtx_hasty ps (box <$> vec_to_list (fp x).(fp_tys)),
+                   tctx_elt_interp tid y) -∗
+    (∀ ret, na_own tid.(tid_na_inv_pool) top -∗ qκs.[lft_intersect_list κs] -∗
+             (box (fp x).(fp_ty)).(ty_own) tid [VVal ret] -∗
+             WP k [of_val ret] in tid.(tid_tid) {{ _, cont_postcondition }}) -∗
+    WP (call: f ps → k) in tid.(tid_tid) {{ _, cont_postcondition }}.
+  Proof.
+    iIntros (HE Hk') "#LFT #HE Htl Hκs Hf Hargs Hk". rewrite -tctx_hasty_val.
+    iApply (type_call_iris' with "LFT HE Htl [] Hκs Hf Hargs [Hk]"); [done..| |].
+    - instantiate (1 := 1%Qp). by rewrite /llctx_interp.
+    - iIntros "* Htl _". iApply "Hk". done.
+  Qed.
+
+  Lemma type_call' E L (κs : list lft) T p (ps : list path)
+                   {A} (fp : A → fn_params (length ps)) (k : val) x :
+    Forall (lctx_lft_alive E L) κs →
+    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) L ((fp x).(fp_E) ϝ)) →
+    typed_body E L [k ◁cont(L, λ v : vec _ 1, (v!!!0 ◁ box (fp x).(fp_ty)) :: T)]
+               ((p ◁ fn fp) ::
+                zip_with TCtx_hasty ps (box <$> vec_to_list (fp x).(fp_tys)) ++
+                T)
+               (call: p ps → k).
+  Proof.
+    iIntros (Hκs HE tid) "#LFT #HE Htl HL HC (Hf & Hargs & HT)".
+    iMod (lctx_lft_alive_tok_list _ _ κs with "HE HL") as (q) "(Hκs & HL & Hclose)"; [done..|].
+    iApply (type_call_iris' with "LFT HE Htl HL Hκs Hf Hargs"); [done|].
+    iIntros (r) "Htl HL Hκs Hret". iMod ("Hclose" with "Hκs HL") as "HL".
+    iSpecialize ("HC" with "[]"); first by (iPureIntro; apply elem_of_list_singleton).
+    iApply ("HC" $! [#r] with "Htl HL").
+    rewrite tctx_interp_cons tctx_hasty_val. iFrame.
+  Qed.
+
+  (* Specialized type_call':  Adapted for use by solve_typing; fixed "list of
+     alive lifetimes" to be the local ones. *)
+  Lemma type_call {A} x E L C T T' T'' p (ps : list path)
+                        (fp : A → fn_params (length ps)) k :
+    p ◁ fn fp ∈ T →
+    Forall (lctx_lft_alive E L) (L.*1) →
+    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> (L.*1)) ++ E) L ((fp x).(fp_E) ϝ)) →
+    tctx_extract_ctx E L (zip_with TCtx_hasty ps
+                                   (box <$> vec_to_list (fp x).(fp_tys))) T T' →
+    k ◁cont(L, T'') ∈ C →
+    (∀ ret : val, tctx_incl E L ((ret ◁ box (fp x).(fp_ty))::T') (T'' [# ret])) →
+    typed_body E L C T (call: p ps → k).
+  Proof.
+    intros Hfn HL HE HTT' HC HT'T''.
+    rewrite -typed_body_mono /flip; last done; first by eapply type_call'.
+    - etrans. eapply (incl_cctx_incl _ [_]); first by intros ? ->%elem_of_list_singleton.
+      apply cctx_incl_cons_match; first done. intros args. by inv_vec args.
+    - etrans; last by apply (tctx_incl_frame_l [_]).
+      apply copy_elem_of_tctx_incl; last done. apply _.
+  Qed.
+
+  Lemma type_letcall {A} x E L C T T' p (ps : list path)
+                        (fp : A → fn_params (length ps)) b e :
+    Closed (b :b: []) e → Closed [] p → Forall (Closed []) ps →
+    p ◁ fn fp ∈ T →
+    Forall (lctx_lft_alive E L) (L.*1) →
+    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> (L.*1)) ++ E) L ((fp x).(fp_E) ϝ)) →
+    tctx_extract_ctx E L (zip_with TCtx_hasty ps
+                                   (box <$> vec_to_list (fp x).(fp_tys))) T T' →
+    (∀ ret : val, typed_body E L C ((ret ◁ box (fp x).(fp_ty))::T') (subst' b ret e)) -∗
+    typed_body E L C T (letcall: b := p ps in e).
+  Proof.
+    iIntros (?? Hpsc ????) "He".
+    iApply (type_cont_norec [_] _ (λ r, (r!!!0 ◁ box (fp x).(fp_ty)) :: T')).
+    - (* TODO : make [solve_closed] work here. *)
+      eapply is_closed_weaken; first done. set_solver+.
+    - (* TODO : make [solve_closed] work here. *)
+      rewrite /Closed /= !andb_True. split.
+      + by eapply is_closed_weaken, list_subseteq_nil.
+      + eapply Is_true_eq_left, forallb_forall, List.Forall_forall, Forall_impl=>//.
+        intros. eapply Is_true_eq_true, is_closed_weaken=>//. set_solver+.
+    - iIntros (k).
+      (* TODO : make [simpl_subst] work here. *)
+      change (subst' "_k" k (p ((λ: ["_r"], (#☠ ;; #☠) ;; "_k" ["_r"])%E :: ps))) with
+             ((subst "_k" k p) ((λ: ["_r"], (#☠ ;; #☠) ;; k ["_r"])%E :: map (subst "_k" k) ps)).
+      rewrite is_closed_nil_subst //.
+      assert (map (subst "_k" k) ps = ps) as ->.
+      { clear -Hpsc. induction Hpsc=>//=. rewrite is_closed_nil_subst //. congruence. }
+      iApply type_call; try done. constructor. done.
+    - simpl. iIntros (k ret). inv_vec ret=>ret. rewrite /subst_v /=.
+      rewrite ->(is_closed_subst []); last set_solver+; last first.
+      { apply subst'_is_closed; last done. apply is_closed_of_val. }
+      (iApply typed_body_mono; last by iApply "He"); [|done..].
+      apply incl_cctx_incl. set_solver+.
+  Qed.
+
+  Lemma type_rec {A} E L fb (argsb : list binder) ef e n
+        (fp : A → fn_params n) T `{!CopyC T, !SendC T, Closed _ e} :
+    IntoVal ef (funrec: fb argsb := e) →
+    n = length argsb →
+    □ (∀ x ϝ (f : val) k (args : vec val (length argsb)),
+          typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ₗ []]
+                     [k ◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
+                     ((f ◁ fn fp) ::
+                        zip_with (TCtx_hasty ∘ of_val) args
+                                 (box <$> vec_to_list (fp x).(fp_tys)) ++ T)
+                     (subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) -∗
+    typed_instruction_ty E L T ef (fn fp).
+  Proof.
+    iIntros (<-%of_to_val ->) "#Hbody". iIntros (tid) "#LFT _ $ $ #HT". iApply wp_value.
+    rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
+    { unlock. rewrite /= decide_left. done. }
+    iExists fb, _, argsb, e, _. iSplit. done. iSplit. done. iNext.
+    iIntros (x ϝ k args) "!#". iIntros (tid') "_ HE Htl HL HC HT'".
+    iApply ("Hbody" with "LFT HE Htl HL HC").
+    rewrite tctx_interp_cons tctx_interp_app. unlock. iFrame "IH HT'".
+    by iApply sendc_change_tid.
+  Qed.
+
+  Lemma type_fn {A} E L (argsb : list binder) ef e n
+        (fp : A → fn_params n) T `{!CopyC T, !SendC T, Closed _ e} :
+    IntoVal ef (funrec: <> argsb := e) →
+    n = length argsb →
+    □ (∀ x ϝ k (args : vec val (length argsb)),
+        typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ₗ []]
+                   [k ◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
+                   (zip_with (TCtx_hasty ∘ of_val) args
+                             (box <$> vec_to_list (fp x).(fp_tys)) ++ T)
+                   (subst_v (BNamed "return" :: argsb) (k ::: args) e)) -∗
+    typed_instruction_ty E L T ef (fn fp).
+  Proof.
+    iIntros (??) "#He". iApply type_rec; try done. iIntros "!# *".
+    iApply typed_body_mono; last iApply "He"; try done.
+    eapply contains_tctx_incl. by constructor.
+  Qed.
+End typing.
+
+Hint Resolve fn_subtype : lrust_typing.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index a8e6713e404f6b2a6e0bfb687ba699179e54418c..ab90cbb1f542c7613fec260b94d7fe9c9beaff9d 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -296,7 +296,7 @@ Section typing.
     iDestruct (ty_size_eq with "Hown") as "#>EQ".
     iDestruct "EQ" as %<-. iApply (wp_delete with "[-]"); auto.
     - iFrame "H↦". rewrite freeable_sz_full. iDestruct "H†" as "[?|%]"; auto.
-    - rewrite /tctx_interp /=. by iIntros "!> _ !>".
+    - rewrite /tctx_interp /=. auto.
   Qed.
 
   Lemma type_delete {E L} ty C T T' (n' : nat) (n : Z)  p e :
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index c13420bd762b2dacc93899f9cb527dc0da3cbbdf..b499d09052ca5a61c8169701f7ad5b9341ac7ad7 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -9,10 +9,10 @@ Section typing.
   (** Function Body *)
   (* This is an iProp because it is also used by the function type. *)
   Definition typed_body (E : elctx) (L : llctx) (C : cctx) (T : tctx)
-                        (e : expr) : tvPropI Σ :=
-    (∀ tid, ⎡lft_ctx⎤ -∗ ⎡elctx_interp E⎤ -∗ ⎡na_own tid ⊤⎤ -∗ ⎡llctx_interp L 1⎤ -∗
-               cctx_interp tid C -∗ ⎡tctx_interp tid T⎤ -∗
-               WP e {{ _, cont_postcondition }})%I.
+                        (e : expr) : vPropI Σ :=
+    (∀ tid, ⎡lft_ctx⎤ -∗ elctx_interp E -∗ na_own tid.(tid_na_inv_pool) ⊤ -∗
+               llctx_interp L 1 -∗ cctx_interp tid C -∗ tctx_interp tid T -∗
+               WP e in tid.(tid_tid) {{ _, cont_postcondition }})%I.
   Global Arguments typed_body _ _ _ _ _%E.
 
   Global Instance typed_body_llctx_permut E :
@@ -47,20 +47,20 @@ Section typing.
 
   (** Instruction *)
   Definition typed_instruction (E : elctx) (L : llctx)
-             (T1 : tctx) (e : expr) (T2 : val → tctx) : tvPropI Σ :=
-    (∀ tid, ⎡lft_ctx⎤ -∗ ⎡elctx_interp E⎤ -∗ ⎡na_own tid ⊤⎤ -∗
-              ⎡llctx_interp L 1⎤ -∗ ⎡tctx_interp tid T1⎤ -∗
-              WP e {{ v, ⎡na_own tid ⊤⎤ ∗
-                         ⎡llctx_interp L 1⎤ ∗ ⎡tctx_interp tid (T2 v)⎤ }})%I.
+             (T1 : tctx) (e : expr) (T2 : val → tctx) : vPropI Σ :=
+    (∀ tid, ⎡lft_ctx⎤ -∗ elctx_interp E -∗ na_own tid.(tid_na_inv_pool) ⊤ -∗
+              llctx_interp L 1 -∗ tctx_interp tid T1 -∗
+       WP e in tid.(tid_tid) {{ v, na_own tid.(tid_na_inv_pool) ⊤ ∗ llctx_interp L 1 ∗
+                                   tctx_interp tid (T2 v) }})%I.
   Global Arguments typed_instruction _ _ _ _%E _.
 
   (** Writing and Reading **)
-  Definition typed_write (E : elctx) (L : llctx) (ty1 ty ty2 : type) : tvPropI Σ :=
+  Definition typed_write (E : elctx) (L : llctx) (ty1 ty ty2 : type) : vPropI Σ :=
     (□ ∀ v tid F qL, ⌜lftE ∪ (↑lrustN) ⊆ F⌝ →
-      ⎡lft_ctx⎤ -∗ ⎡elctx_interp E⎤ -∗ ⎡llctx_interp L qL⎤ -∗ ⎡ty1.(ty_own) tid [v]⎤ ={F}=∗
-        ∃ (l : loc) vl, ⌜length vl = ty.(ty_size) ∧ v = VVal #l⌝ ∗ ⎡l ↦∗ vl⎤ ∗
-          (⎡▷ l ↦∗: ty.(ty_own) tid⎤ ={F}=∗
-            ⎡llctx_interp L qL⎤ ∗ ⎡ty2.(ty_own) tid [v]⎤))%I.
+      ⎡lft_ctx⎤ -∗ elctx_interp E -∗ llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
+        ∃ (l : loc) vl, ⌜length vl = ty.(ty_size) ∧ v = VVal #l⌝ ∗ l ↦∗ vl ∗
+          (▷ l ↦∗: ty.(ty_own) tid ={F}=∗
+            llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
   Global Arguments typed_write _ _ _%T _%T _%T.
 
   (* Technically speaking, we could remvoe the vl quantifiaction here and use
@@ -68,18 +68,18 @@ Section typing.
      make work for some of the provers way harder, since they'd have to show
      that nobody could possibly have changed the vl (because only half the
      fraction was given). So we go with the definition that is easier to prove. *)
-  Definition typed_read (E : elctx) (L : llctx) (ty1 ty ty2 : type) : tvPropI Σ :=
+  Definition typed_read (E : elctx) (L : llctx) (ty1 ty ty2 : type) : vPropI Σ :=
     (□ ∀ v tid F qL, ⌜lftE ∪ ↑lrustN ⊆ F⌝ →
-      ⎡lft_ctx⎤ -∗ ⎡elctx_interp E⎤ -∗ ⎡na_own tid F⎤ -∗
-      ⎡llctx_interp L qL⎤ -∗ ⎡ty1.(ty_own) tid [v]⎤ ={F}=∗
-        ∃ (l : loc) vl q, ⌜v = VVal #l⌝ ∗ ⎡l ↦∗{q} vl⎤ ∗ ⎡▷ ty.(ty_own) tid vl⎤ ∗
-              (⎡l ↦∗{q} vl⎤ ={F}=∗ ⎡na_own tid F⎤ ∗
-                              ⎡llctx_interp L qL⎤ ∗ ⎡ty2.(ty_own) tid [v]⎤))%I.
+      ⎡lft_ctx⎤ -∗ elctx_interp E -∗ na_own tid.(tid_na_inv_pool) F -∗
+      llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
+        ∃ (l : loc) vl q, ⌜v = VVal #l⌝ ∗ l ↦∗{q} vl ∗ ▷ ty.(ty_own) tid vl ∗
+              (l ↦∗{q} vl ={F}=∗ na_own tid.(tid_na_inv_pool) F ∗
+                              llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
   Global Arguments typed_read _ _ _%T _%T _%T.
 End typing.
 
 Definition typed_instruction_ty `{typeG Σ} (E : elctx) (L : llctx) (T : tctx)
-    (e : expr) (ty : type) : tvPropI Σ :=
+    (e : expr) (ty : type) : vPropI Σ :=
   typed_instruction E L T e (λ v, [v ◁ ty]).
 Arguments typed_instruction_ty {_ _} _ _ _ _%E _%T.
 
@@ -168,8 +168,8 @@ Section typing_rules.
     iIntros (Hc Hub) "He". iIntros (tid) "#LFT #HE Htl [Hκ HL] HC HT".
     iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
     iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
-    iApply (wp_mask_mono (↑lftN)); first done.
-    iApply (wp_step_fupd _ ∅ with "[Hend]"); [done|set_solver| |].
+    iApply (wp_mask_mono _ (↑lftN)); first done.
+    iApply (wp_step_fupd _ _ ∅ with "[Hend]"); [done|set_solver| |].
     { iMod "Hend". iModIntro. iNext. iMod "Hend". iModIntro. iApply "Hend". }
     wp_seq. iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT HE Htl HL HC [> -]").
     iMod (Hub with "[] HT") as "$"; [|done]. simpl in *. subst κ.
@@ -228,7 +228,7 @@ Section typing_rules.
         (l vl q [= ->]) "(Hl & Hown & Hclose)"; first done.
     iDestruct (ty_size_eq with "Hown") as "#>%". rewrite ->Hsz in *.
     destruct vl as [|v [|]]; try done.
-    rewrite own_loc_na_vec_singleton. iApply wp_fupd. admit. (*  wp_read. *)
+    rewrite own_loc_na_vec_singleton. iApply wp_fupd. (*  wp_read. *)
     (* iMod ("Hclose" with "Hl") as "($ & $ & Hown2)". *)
     (* rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //. *)
     (* by iFrame. *)
@@ -246,11 +246,11 @@ Section typing_rules.
   Lemma type_memcpy_iris E L qL tid ty ty1 ty1' ty2 ty2' (n : Z) p1 p2 :
     Z.of_nat (ty.(ty_size)) = n →
     typed_write E L ty1 ty ty1' -∗ typed_read E L ty2 ty ty2' -∗
-    {{{ ⎡lft_ctx⎤ ∗ ⎡elctx_interp E⎤ ∗ ⎡na_own tid ⊤⎤ ∗ ⎡llctx_interp L qL⎤ ∗
-        ⎡tctx_elt_interp tid (p1 ◁ ty1)⎤ ∗ ⎡tctx_elt_interp tid (p2 ◁ ty2)⎤ }}}
-      (p1 <-{n} !p2)
-    {{{ RET #☠; ⎡na_own tid ⊤⎤ ∗ ⎡llctx_interp L qL⎤ ∗
-                 ⎡tctx_elt_interp tid (p1 ◁ ty1')⎤ ∗ ⎡tctx_elt_interp tid (p2 ◁ ty2')⎤ }}}.
+    {{{ ⎡lft_ctx⎤ ∗ elctx_interp E ∗ na_own tid.(tid_na_inv_pool) ⊤ ∗ llctx_interp L qL ∗
+        tctx_elt_interp tid (p1 ◁ ty1) ∗ tctx_elt_interp tid (p2 ◁ ty2) }}}
+      (p1 <-{n} !p2) in tid.(tid_tid)
+    {{{ RET #☠; na_own tid.(tid_na_inv_pool) ⊤ ∗ llctx_interp L qL ∗
+                 tctx_elt_interp tid (p1 ◁ ty1') ∗ tctx_elt_interp tid (p2 ◁ ty2') }}}.
   Proof.
     iIntros (<-) "#Hwrt #Hread !#".
     iIntros (Φ) "(#LFT & #HE & Htl & [HL1 HL2] & [Hp1 Hp2]) HΦ".
@@ -279,7 +279,7 @@ Section typing_rules.
     { iApply Hwrt. }
     { iApply Hread. }
     { rewrite tctx_interp_cons tctx_interp_singleton. by iDestruct "HT" as "[$$]". }
-    rewrite tctx_interp_cons tctx_interp_singleton embed_sep. auto.
+    rewrite tctx_interp_cons tctx_interp_singleton. auto.
   Qed.
 
   Lemma type_memcpy {E L} ty ty1 ty2 (n : Z) C T T' ty1' ty2' p1 p2 e:
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 989e0dc3a2917ab58dd134c1fd3cd5303f5234d4..3e2f936c6eb2c3a03f0b8c2057267c89028a5a30 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -15,7 +15,9 @@ Definition lftE : coPset := ↑lftN.
 Definition lrustN := nroot .@ "lrust".
 Definition shrN  := lrustN .@ "shr".
 
-Definition thread_id := na_inv_pool_name.
+Record thread_id :=
+  { tid_na_inv_pool : na_inv_pool_name;
+    tid_tid : gname }.
 
 Record type `{typeG Σ} :=
   { ty_size : nat;
@@ -392,11 +394,11 @@ Class Copy `{typeG Σ} (t : type) := {
   copy_persistent tid vl : Persistent (t.(ty_own) tid vl);
   copy_shr_acc κ tid E F l q :
     lftE ∪ ↑shrN ⊆ E → shr_locsE l (t.(ty_size) + 1) ⊆ F →
-    ⎡lft_ctx⎤ -∗ t.(ty_shr) κ tid l -∗ na_own tid F -∗ q.[κ] ={E}=∗
-       ∃ q', na_own tid (F ∖ shr_locsE l t.(ty_size)) ∗
+    ⎡lft_ctx⎤ -∗ t.(ty_shr) κ tid l -∗ na_own tid.(tid_na_inv_pool) F -∗ q.[κ] ={E}=∗
+       ∃ q', na_own tid.(tid_na_inv_pool) (F ∖ shr_locsE l t.(ty_size)) ∗
          ▷(l ↦∗{q'}: t.(ty_own) tid) ∗
-      (na_own tid (F ∖ shr_locsE l t.(ty_size)) -∗ ▷l ↦∗{q'}: t.(ty_own) tid
-                                  ={E}=∗ na_own tid F ∗ q.[κ])
+      (na_own tid.(tid_na_inv_pool) (F ∖ shr_locsE l t.(ty_size)) -∗
+         ▷l ↦∗{q'}: t.(ty_own) tid ={E}=∗ na_own tid.(tid_na_inv_pool) F ∗ q.[κ])
 }.
 Existing Instances copy_persistent.
 Instance: Params (@Copy) 2.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 37fc109d980d53639431430076ebdb8e0918d261..5529869ef041942301faf60ac4d9a38d1eb2be3c 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -36,8 +36,8 @@ Section type_context.
     eval_path v = Some v.
   Proof. destruct v. done. simpl. rewrite (decide_left _). done. Qed.
 
-  Lemma wp_eval_path E p v :
-    eval_path p = Some v → (WP p @ E {{ v', ⌜v' = v⌝ }})%I.
+  Lemma wp_eval_path E tid p v :
+    eval_path p = Some v → (WP p in tid @ E {{ v', ⌜v' = v⌝ }})%I.
   Proof.
     revert v; induction p; intros v; cbn -[to_val];
       try (simpl; intros ?; simplify_eq; by iApply wp_value).
@@ -95,9 +95,9 @@ Section type_context.
   Qed.
 
   Lemma wp_hasty E tid p ty Φ :
-    ⎡tctx_elt_interp tid (p ◁ ty)⎤ -∗
-    (∀ v, ⌜eval_path p = Some v⌝ -∗ ⎡ty.(ty_own) tid [VVal v]⎤ -∗ Φ v) -∗
-    WP p @ E {{ Φ }}.
+    tctx_elt_interp tid (p ◁ ty) -∗
+    (∀ v, ⌜eval_path p = Some v⌝ -∗ ty.(ty_own) tid [VVal v] -∗ Φ v) -∗
+    WP p in tid.(tid_tid) @ E {{ Φ }}.
   Proof.
     iIntros "Hty HΦ". iDestruct "Hty" as (v) "[% Hown]".
     iApply (wp_wand with "[]"). { iApply wp_eval_path. done. }
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index a0cb35a52386f199911a9ef42bfdae8976cdc0d2..e2e969c44e8cb9cd73812fe1fc3abe2ea3e0087d 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -42,8 +42,7 @@ Section case.
     - rewrite /= -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
       iExists (VVal #i :: vl' ++ vl''). iNext.
       rewrite own_loc_na_vec_cons own_loc_na_vec_app.
-      iFrame. iExists i, vl', vl''. rewrite /= app_length nth_lookup EQty /=.
-      iModIntro. auto.
+      iFrame. iExists i, vl', vl''. rewrite /= app_length nth_lookup EQty /=. auto.
   Qed.
 
   Lemma type_case_own E L C T T' p n tyl el :
@@ -80,7 +79,7 @@ Section case.
     destruct Hety as [Hety|Hety].
     - iMod ("Hclose'" $! ((l >> 1) ↦∗: ty.(ty_own) tid)%I
             with "[H↦i H↦vl''] [H↦vl' Hown]") as "[Hb Htok]".
-      { iIntros "!>!>Hown". iDestruct "Hown" as (vl'2) "[H↦ Hown]".
+      { iIntros "!>Hown". iDestruct "Hown" as (vl'2) "[H↦ Hown]".
         iExists (VVal #i::vl'2++vl''). iIntros "!>". iNext.
         iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'2.
         rewrite own_loc_na_vec_cons own_loc_na_vec_app EQlenvl' EQlenvl'2.
@@ -91,10 +90,10 @@ Section case.
       iApply (Hety with "LFT HE Hna HL HC").
       rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame.
     - iMod ("Hclose'" with "[] [H↦i H↦vl' H↦vl'' Hown]") as "[Hb Htok]";
-        [by iIntros "!>!>$"| |].
+        [by iIntros "!>$"| |].
       { iExists (VVal #i::vl'++vl'').
         rewrite own_loc_na_vec_cons own_loc_na_vec_app /= -EQlen. iFrame. iNext.
-        iExists i, vl', vl''. rewrite nth_lookup EQty. iModIntro. auto. }
+        iExists i, vl', vl''. rewrite nth_lookup EQty. auto. }
       iMod ("Hclose" with "Htok") as "HL".
       iApply (Hety with "LFT HE Hna HL HC").
       rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame.
@@ -130,7 +129,7 @@ Section case.
     iMod ("Hclose" with "Htok") as "HL".
     destruct Hety as [Hety|Hety]; iApply (Hety with "LFT HE Hna HL HC");
       rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //; iFrame.
-    iExists _. rewrite ->nth_lookup, EQty. iModIntro. auto.
+    iExists _. rewrite ->nth_lookup, EQty. auto.
   Qed.
 
   Lemma type_case_shr E L C T p κ tyl el :
@@ -166,7 +165,7 @@ Section case.
     rewrite own_loc_na_vec_cons -wp_fupd. iDestruct "H↦vl" as "[H↦ H↦vl]". wp_write.
     rewrite tctx_interp_singleton tctx_hasty_val' //. iApply "Hw". iNext.
     iExists (_::_::_). rewrite !own_loc_na_vec_cons. iFrame.
-    iExists i, [_], _. rewrite -Hlen nth_lookup Hty. iModIntro. auto.
+    iExists i, [_], _. rewrite -Hlen nth_lookup Hty. auto.
   Qed.
 
   Lemma type_sum_assign {E L} sty tyl i ty1 ty ty1' C T T' p1 p2 e: