diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 0f6eee225eaa64c51f341e1874cd7ed6e17a819b..db1825ad8540ed93b416432e38195bc98e22b88a 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -16,6 +16,8 @@ Section bool.
   Next Obligation. intros ? [|[[| |[|[]|]]|] []]; auto. Qed.
   Next Obligation. intros ? [|[[| |[|[]|]]|] []]; apply _. Qed.
 
+  Global Instance bool_wf : TyWf bool := { ty_lfts := []; ty_wf_E := [] }.
+
   Global Instance bool_send : Send bool.
   Proof. done. Qed.
 End bool.
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 909052bcdc274fd99d7c0a7c3ccc5641cd2fd2c6..0c0d96edc86b3123cd613ed419cf68c9759ba101 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -12,7 +12,7 @@ Section get_x.
        delete [ #1; "p"] ;; "return" ["r"].
 
   Lemma get_x_type :
-    typed_val 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. *)
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index 2d33668a9e052ffcaee7555a610d51d7503adad4..b13fe440196806f1c38bfedbcf66829ee1d02589 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -12,8 +12,7 @@ Section init_prod.
        "r" +â‚— #0 <- "x'";; "r" +â‚— #1 <- "y'";;
        delete [ #1; "x"] ;; delete [ #1; "y"] ;; return: ["r"].
 
-  Lemma init_prod_type :
-    typed_val init_prod (fn(λ ϝ, []; int, int) → Π[int;int]).
+  Lemma init_prod_type : typed_val init_prod (fn(∅; int, int) → Π[int;int]).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([] ϝ ret p). inv_vec p=>x y. simpl_subst.
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 75e581ca15842c709403117d6e126672aae32504..12d8c2956bdb76cb7b855ca3091aa544028a62cb 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -17,8 +17,7 @@ Section lazy_lft.
       let: "r" := new [ #0] in
       Endlft;; delete [ #2; "t"];; delete [ #1; "f"];; delete [ #1; "g"];; "return" ["r"].
 
-  Lemma lazy_lft_type :
-    typed_val lazy_lft (fn(λ ϝ, []) → unit).
+  Lemma lazy_lft_type : typed_val lazy_lft (fn(∅) → unit).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([] ϝ ret p). inv_vec p. simpl_subst.
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index f098582d4276886ff733e26c0186741df82098b0..a434296c11933105dcd57600436714d10dee3752 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -17,7 +17,7 @@ Section rebor.
                  delete [ #1; "x"] ;; "return" ["r"].
 
   Lemma rebor_type :
-    typed_val rebor (fn(λ ϝ, []; Π[int; int], Π[int; int]) → int).
+    typed_val rebor (fn(∅; Π[int; int], Π[int; int]) → int).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([] ϝ ret p). inv_vec p=>t1 t2. simpl_subst.
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index 07049ade01b1ed58f38f0afc64d47d28140e1777..586e2aa81acde2265196dfdbda8e103df23dead6 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -12,7 +12,7 @@ Section unbox.
        delete [ #1; "b"] ;; "return" ["r"].
 
   Lemma ubox_type :
-    typed_val unbox (fn(∀ α, λ ϝ, [ϝ ⊑ α]; &uniq{α}box (Π[int; int])) → &uniq{α} int).
+    typed_val unbox (fn(∀ α, ∅; &uniq{α}box (Π[int; int])) → &uniq{α} int).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret b). inv_vec b=>b. simpl_subst.
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index a3bd0cc24ae67cd40d821e75ada9f928408506f6..847cac84d96b4b11dd024a849054751ac6d5e654 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -16,6 +16,25 @@ Section fixpoint_def.
   Qed.
 
   Definition type_fixpoint : type := fixpointK 2 T.
+
+  (* The procedure for computing ty_lfts and ty_wf_E for fixpoints is
+     the following:
+       - We do a first pass for computing [ty_lfts].
+       - In a second pass, we compute [ty_wf_E], by using the result of the
+         first pass.
+     I believe this gives the right sets for all types that we can define in
+     Rust, but I do not have any proof of this.
+     TODO : investigate this in more detail. *)
+  Global Instance type_fixpoint_wf `{∀ `{!TyWf ty}, TyWf (T ty)} : TyWf type_fixpoint :=
+    let lfts :=
+      let _ : TyWf type_fixpoint := {| ty_lfts := []; ty_wf_E := [] |} in
+      (T type_fixpoint).(ty_lfts)
+    in
+    let wf_E :=
+      let _ : TyWf type_fixpoint := {| ty_lfts := lfts; ty_wf_E := [] |} in
+      (T type_fixpoint).(ty_wf_E)
+    in
+    {| ty_lfts := lfts; ty_wf_E := wf_E |}.
 End fixpoint_def.
 
 Lemma type_fixpoint_ne `{typeG Σ} (T1 T2 : type → type)
diff --git a/theories/typing/function.v b/theories/typing/function.v
index a2cfc11c399dfeeb483f537bd1ae00e04ef692d6..b788a6002b5718dda5c2507d02d3f26030c54008 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -8,7 +8,12 @@ Set Default Proof Using "Type".
 Section fn.
   Context `{typeG Σ} {A : Type} {n : nat}.
 
-  Record fn_params := FP' { fp_tys : vec type n; fp_ty : type; fp_E : lft → elctx }.
+  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.
 
   Program Definition fn (fp : A → fn_params) : type :=
     {| st_own tid vl := (∃ fb kb xb e H,
@@ -23,6 +28,14 @@ Section fn.
     iIntros (fp tid vl) "H". iDestruct "H" as (fb kb xb e ?) "[% _]". by subst.
   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.
 
@@ -47,8 +60,9 @@ Section fn.
   Proof. intros ?? HR ??->. apply HR. Qed.
 
   Global Instance FP_proper R :
-    Proper (flip (Forall2 R : relation (vec _ _)) ==> R ==>
-            pointwise_relation lft eq ==> fn_params_rel R) FP'.
+    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' :
@@ -98,12 +112,6 @@ End fn.
 
 Arguments fn_params {_ _} _.
 
-(* The parameter of [FP'] are in the wrong order in order to make sure
-   that type-checking is done in that order, so that the [ELCtx_Alive]
-   is taken as a coercion. We reestablish the intuitive order with
-   [FP] *)
-Notation FP E tys ty := (FP' tys ty E).
-
 (* 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
@@ -112,22 +120,24 @@ Notation FP E tys ty := (FP' tys ty E).
    printing. Once on 8.6pl1, this should work.  *)
 Notation "'fn(∀' x .. x' ',' E ';' T1 ',' .. ',' TN ')' '→' R" :=
   (fn (λ x, (.. (λ x',
-      FP E%EL (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T R%T)..)))
+      FP_wf E%EL (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T 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 E%EL Vector.nil R%T)..)))
+  (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 E%EL (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..) R%T))
+  (fn (λ _:(), FP_wf E%EL (Vector.cons T1 .. (Vector.cons TN 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 E%EL Vector.nil R%T))
+  (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 Σ}.
 
@@ -191,7 +201,7 @@ Section typing.
   Proof.
     intros fp1 fp2 Hfp. apply fn_subtype=>x ϝ. destruct (Hfp x) as (Htys & Hty & HE).
     split; last split.
-    - rewrite (HE ϝ). apply elctx_sat_app_weaken_l, elctx_sat_refl.
+    - 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.
@@ -202,11 +212,11 @@ Section typing.
             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 ϝ). apply elctx_sat_app_weaken_l, elctx_sat_refl.
+    - 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 ϝ). apply elctx_sat_app_weaken_l, elctx_sat_refl.
+    - 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.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 520901b94ee0d9588d9778869f92766bfbdf378e..93e879cea9ae6f6e8aba338e644cc2aadb895f68 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -15,6 +15,8 @@ Section int.
   Next Obligation. intros ? [|[[]|] []]; auto. Qed.
   Next Obligation. intros ? [|[[]|] []]; apply _. Qed.
 
+  Global Instance int_wf : TyWf int := { ty_lfts := []; ty_wf_E := [] }.
+
   Global Instance int_send : Send int.
   Proof. done. Qed.
 End int.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 6ad7b8d070e30ba9b86a224c1f15303fb68aeff2..5c16ddf563a8ffb4d201b6f695b279951daf6612 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -114,6 +114,9 @@ Section lft_contexts.
   Definition lctx_lft_eq κ κ' : Prop :=
     lctx_lft_incl κ κ' ∧ lctx_lft_incl κ' κ.
 
+  Lemma lctx_lft_incl_incl κ κ' : lctx_lft_incl κ κ' → lctx_lft_incl κ κ'.
+  Proof. done. Qed.
+
   Lemma lctx_lft_incl_relf κ : lctx_lft_incl κ κ.
   Proof. iIntros (qL) "_ !# _". iApply lft_incl_refl. Qed.
 
@@ -300,26 +303,12 @@ Arguments lctx_lft_incl {_ _ _} _%EL _%LL _ _.
 Arguments lctx_lft_eq {_ _ _} _%EL _%LL _ _.
 Arguments lctx_lft_alive {_ _ _} _%EL _%LL _.
 Arguments elctx_sat {_ _ _} _%EL _%LL _%EL.
+Arguments lctx_lft_incl_incl {_ _ _ _%EL _%LL} _ _.
 Arguments lctx_lft_alive_tok {_ _ _ _%EL _%LL} _ _ _.
 
-Lemma elctx_sat_cons_weaken `{invG Σ, lftG Σ} e0 E E' L :
-  elctx_sat E L E' → elctx_sat (e0 :: E) L E'.
-Proof.
-  iIntros (HE' ?) "HL". iDestruct (HE' with "HL") as "#HE'".
-  iClear "∗". iIntros "!# #[_ HE]". iApply "HE'". done.
-Qed.
-
-Lemma elctx_sat_app_weaken_l `{invG Σ, lftG Σ} E0 E E' L :
-  elctx_sat E L E' → elctx_sat (E0 ++ E) L E'.
-Proof. induction E0=>//= ?. auto using elctx_sat_cons_weaken. Qed.
-
-Lemma elctx_sat_app_weaken_r `{invG Σ, lftG Σ} E0 E E' L :
-  elctx_sat E L E' → elctx_sat (E ++ E0) L E'.
-Proof.
-  intros ?. rewrite /elctx_sat /elctx_interp.
-  setoid_rewrite (big_opL_permutation _ (E++E0)); try apply Permutation_app_comm.
-  by apply elctx_sat_app_weaken_l.
-Qed.
+Lemma elctx_sat_submseteq `{invG Σ, lftG Σ} E E' L :
+  E' ⊆+ E → elctx_sat E L E'.
+Proof. iIntros (HE' ?) "_ !# H". by iApply big_sepL_submseteq. Qed.
 
 Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
 Hint Resolve of_val_unlock : lrust_typing.
@@ -328,8 +317,15 @@ Hint Resolve
      lctx_lft_incl_external'
      lctx_lft_alive_static lctx_lft_alive_local lctx_lft_alive_external
      elctx_sat_nil elctx_sat_lft_incl elctx_sat_app elctx_sat_refl
+     submseteq_cons submseteq_inserts_l submseteq_inserts_r
   : lrust_typing.
-Hint Resolve elctx_sat_cons_weaken elctx_sat_app_weaken_l elctx_sat_app_weaken_r
-             | 100 : lrust_typing.
+
+Hint Resolve elctx_sat_submseteq | 100 : lrust_typing.
+
+(* FIXME : I would prefer using a [Hint Resolve <-] for this, but
+   unfortunately, this is not preserved across modules. See:
+     https://coq.inria.fr/bugs/show_bug.cgi?id=5189
+   This should be fixed in the next version of Coq. *)
+Hint Extern 1 (_ ∈ _ ++ _) => apply <- @elem_of_app : lrust_typing.
 
 Hint Opaque elctx_sat lctx_lft_alive lctx_lft_incl : lrust_typing.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 06c092adf1b1337d05d378263332ad861e949e84..1de6c057ffc02905d1993707608fe1f4b843c84f 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -21,6 +21,9 @@ Section cell.
     iIntros (ty ?? tid l) "#H⊑ H". by iApply (na_bor_shorten with "H⊑").
   Qed.
 
+  Global Instance cell_wf ty `{!TyWf ty} : TyWf (cell ty) :=
+    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
   Global Instance cell_type_ne : TypeNonExpansive cell.
   Proof. solve_type_proper. Qed.
 
@@ -85,8 +88,7 @@ Section typing.
   (* Constructing a cell. *)
   Definition cell_new : val := funrec: <> ["x"] := return: ["x"].
 
-  Lemma cell_new_type ty :
-    typed_val cell_new (fn(λ _, []; ty) → cell ty).
+  Lemma cell_new_type ty `{!TyWf ty} : typed_val cell_new (fn(∅; ty) → cell ty).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -97,8 +99,8 @@ Section typing.
   (* The other direction: getting ownership out of a cell. *)
   Definition cell_into_inner : val := funrec: <> ["x"] := return: ["x"].
 
-  Lemma cell_into_inner_type ty :
-    typed_val cell_into_inner (fn(λ _, []; cell ty) → ty).
+  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 "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -109,8 +111,8 @@ Section typing.
   Definition cell_get_mut : val :=
     funrec: <> ["x"] := return: ["x"].
 
-  Lemma cell_get_mut_type ty :
-    typed_val cell_get_mut (fn(∀ α, λ ϝ, [ϝ ⊑ α]; &uniq{α} (cell ty)) → &uniq{α} ty).
+  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 "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -126,8 +128,8 @@ Section typing.
       letalloc: "r" <-{ty.(ty_size)} !"x'" in
       delete [ #1; "x"];; return: ["r"].
 
-  Lemma cell_get_type `(!Copy ty) :
-    typed_val (cell_get ty) (fn(∀ α, λ ϝ, [ϝ ⊑ α]; &shr{α} (cell ty)) → ty).
+  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 "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -146,8 +148,8 @@ Section typing.
       "c'" <-{ty.(ty_size)} !"x";;
       delete [ #1; "c"] ;; delete [ #ty.(ty_size); "x"] ;; return: ["r"].
 
-  Lemma cell_replace_type ty :
-    typed_val (cell_replace ty) (fn(∀ α, λ ϝ, [ϝ ⊑ α]; &shr{α} cell ty, ty) → ty).
+  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 "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>c x. simpl_subst.
diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
index 2d5487ed2c11bff63da83a4089793f59a1d458c7..f25234813054d7fa35f008316fd2bb07b67de976 100644
--- a/theories/typing/lib/fake_shared_box.v
+++ b/theories/typing/lib/fake_shared_box.v
@@ -9,17 +9,15 @@ Section fake_shared_box.
   Definition fake_shared_box : val :=
     funrec: <> ["x"] := Skip ;; return: ["x"].
 
-  Lemma cell_replace_type ty :
+  Lemma fake_shared_box_type ty `{!TyWf ty} :
     typed_val fake_shared_box
-      (fn (fun '(α, β) => FP (λ ϝ, [ϝ ⊑ α; α ⊑ β]%EL)
-                              [# &shr{α}(&shr{β} ty)] (&shr{α}box ty))).
+      (fn (fun '(α, β) => FP_wf ∅ [# &shr{α}(&shr{β} ty)] (&shr{α}box ty))).
   Proof.
     intros. 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.
-    rewrite {1}/elctx_interp big_sepL_cons big_sepL_singleton.
-    iDestruct "HE" as "(Hβ & #Hαβ)".
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
     iAssert (▷ ty_own (own_ptr 1 (&shr{α} box ty)) tid [x])%I with "[HT]" as "HT".
     { destruct x as [[|l|]|]=>//=. iDestruct "HT" as "[H $]".
       iNext. iDestruct "H" as ([|[[]|][]]) "[H↦ H]"; try done.
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 68ab6ea00e1bcfc7fb95b2d14f6a46750c2f1e6b..9b6594b0a530baed23f97f47f3246f46996156e2 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -22,9 +22,9 @@ Section option.
     cont: "k" [] :=
       delete [ #1; "o"];; return: ["r"].
 
-  Lemma option_as_mut_type Ï„ :
+  Lemma option_as_mut_type Ï„ `{!TyWf Ï„} :
     typed_val
-      option_as_mut (fn(∀ α, (λ ϝ, [ϝ ⊑ α]); &uniq{α} (option τ)) → option (&uniq{α}τ)).
+      option_as_mut (fn(∀ α, ∅; &uniq{α} (option τ)) → option (&uniq{α}τ)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
       inv_vec p=>o. simpl_subst.
@@ -53,8 +53,8 @@ Section option.
         delete [ #(S Ï„.(ty_size)); "o"];; delete [ #Ï„.(ty_size); "def"];;
         return: ["r"]].
 
-  Lemma option_unwrap_or_type Ï„ :
-    typed_val (option_unwrap_or τ) (fn((λ ϝ, []); option τ, τ) → τ).
+  Lemma option_unwrap_or_type Ï„ `{!TyWf Ï„} :
+    typed_val (option_unwrap_or τ) (fn(∅; option τ, τ) → τ).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([] ϝ ret p). inv_vec p=>o def. simpl_subst.
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index ccb80f73b5a3b0f687a65e1cfac16511a7a76205..68759c9e8ac1c21fdd0f504a8192562647a5cf47 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -89,10 +89,13 @@ Section rc.
       iModIntro. iNext. iAssert X with "[>HP]" as "HX".
       { iDestruct "HP" as "[[Hl' [H† Hown]]|$]"; last done.
         iMod (lft_create with "LFT") as (ν) "[[Hν1 Hν2] #Hν†]"; first solve_ndisj.
-        (* TODO: We should consider changing the statement of bor_create to dis-entangle the two masks such that this is no longer necessary. *)
+        (* TODO: We should consider changing the statement of
+           bor_create to dis-entangle the two masks such that this is no
+          longer necessary. *)
         iApply (fupd_mask_mono (↑lftN)); first solve_ndisj.
         iMod (bor_create with "LFT Hown") as "[HP HPend]"; first solve_ndisj.
-        iMod (own_alloc (● Some ((1/2)%Qp, 1%positive) ⋅ ◯ Some ((1/2)%Qp, 1%positive))) as (γ) "[Ha Hf]".
+        iMod (own_alloc (● Some ((1/2)%Qp, 1%positive) ⋅
+                         ◯ Some ((1/2)%Qp, 1%positive))) as (γ) "[Ha Hf]".
         { apply auth_valid_discrete_2. done. }
         iMod (na_inv_alloc tid _ _ (rc_inv tid ν γ l' ty) with "[Ha Hν2 Hl' H† HPend]").
         { rewrite /rc_inv. iExists (Some (_, _)). iFrame. iExists _. iFrame "#∗".
@@ -134,6 +137,9 @@ Section rc.
     - by iApply na_bor_shorten.
   Qed.
 
+  Global Instance rc_wf ty `{!TyWf ty} : TyWf (rc ty) :=
+    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
   Global Instance rc_type_contractive : TypeContractive rc.
   Proof.
     constructor;
@@ -148,8 +154,10 @@ Section rc.
   Lemma rc_subtype ty1 ty2 :
     type_incl ty1 ty2 -∗ type_incl (rc ty1) (rc ty2).
   Proof.
-    iIntros "#Hincl". iPoseProof "Hincl" as "Hincl2". iDestruct "Hincl2" as "(#Hsz & #Hoincl & #Hsincl)".
-    (* FIXME: Would be nice to have an easier way to duplicate destructed things.  Maybe iPoseProof with a destruct pattern? *)
+    iIntros "#Hincl". iPoseProof "Hincl" as "Hincl2".
+    iDestruct "Hincl2" as "(#Hsz & #Hoincl & #Hsincl)".
+    (* FIXME: Would be nice to have an easier way to duplicate
+       destructed things.  Maybe iPoseProof with a destruct pattern? *)
     iSplit; first done. iSplit; iAlways.
     - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       iDestruct "Hvl" as "[(Hl & H† & Hc) | Hvl]".
@@ -178,7 +186,6 @@ Section rc.
   Global Instance rc_proper E L :
     Proper (eqtype E L ==> eqtype E L) rc.
   Proof. intros ??[]. by split; apply rc_mono. Qed.
-
 End rc.
 
 Section code.
@@ -247,8 +254,8 @@ Section code.
       "rc" +â‚— #0 <- "rcbox";;
       delete [ #ty.(ty_size); "x"];; return: ["rc"].
 
-  Lemma rc_new_type ty :
-    typed_val (rc_new ty) (fn(λ _, []; ty) → rc ty).
+  Lemma rc_new_type ty `{!TyWf ty} :
+    typed_val (rc_new ty) (fn(∅; ty) → rc ty).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -286,8 +293,8 @@ Section code.
       "rc2" <- "rc''";;
       delete [ #1; "rc" ];; return: ["rc2"].
 
-  Lemma rc_clone_type ty :
-    typed_val rc_clone (fn(∀ α, λ ϝ, [ϝ ⊑ α]; &shr{α} rc ty) → rc ty).
+  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 "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -326,7 +333,7 @@ Section code.
     iMod ("Hclose3" with "[$Hrctok] Hna") as "[Hα1 Hna]".
     iMod ("Hclose2" with "[Hrc● Hl' Hl'† Hνtok2 Hν† $Hna]") as "Hna".
     { iExists _. iFrame "Hrc●". iExists _. rewrite Z.add_comm. iFrame "∗ Hνend".
-      rewrite [_ â‹… _]comm frac_op' -assoc Qp_div_2. auto. }
+      rewrite [_ â‹… _]comm frac_op' -[(_ + _)%Qp]assoc. rewrite Qp_div_2. auto. }
     iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
     (* Finish up the proof. *)
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); #lrc2 ◁ box (rc ty)]%TC
@@ -345,8 +352,8 @@ Section code.
       "x" <- (!"rc'" +â‚— #1);;
       delete [ #1; "rc" ];; return: ["x"].
 
-  Lemma rc_deref_type ty :
-    typed_val rc_deref (fn(∀ α, λ ϝ, [ϝ ⊑ α]; &shr{α} rc ty) → &shr{α} ty).
+  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 "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
@@ -395,8 +402,8 @@ Section code.
     cont: "k" [] :=
       delete [ #1; "rc"];; return: ["r"].
 
-  Lemma rc_try_unwrap_type ty :
-    typed_val (rc_try_unwrap ty) (fn(λ _, []; rc ty) → Σ[ ty; rc ty ]).
+  Lemma rc_try_unwrap_type ty `{!TyWf ty} :
+    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 "/= !#".
@@ -463,8 +470,8 @@ Section code.
     cont: "k" [] :=
       delete [ #1; "rc"];; return: ["x"].
 
-  Lemma rc_drop_type ty :
-    typed_val (rc_drop ty) (fn(λ _, []; rc ty) → option ty).
+  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 "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
@@ -534,8 +541,8 @@ Section code.
     cont: "k" [] :=
       delete [ #1; "rc"];; return: ["x"].
 
-  Lemma rc_get_mut_type ty :
-    typed_val rc_get_mut (fn(∀ α, λ ϝ, [ϝ ⊑ α]; &uniq{α} rc ty) → option (&uniq{α} ty)).
+  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 "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index 785cf6af06d88169f4470f451a8323d6fdfe96d3..dfa8aec05845124e3622da049d188f0d1284ee46 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -68,6 +68,9 @@ Section ref.
     - by iApply na_bor_shorten.
   Qed.
 
+  Global Instance ref_wf α ty `{!TyWf ty} : TyWf (ref α ty) :=
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+
   Global Instance ref_type_contractive α : TypeContractive (ref α).
   Proof. solve_type_proper. Qed.
   Global Instance ref_ne α : NonExpansive (ref α).
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index e71822aeeae6bce95fef5cce9c7949a024bfd486..9f7c86c5f962b1c34d186195e7e9ccdd8793fcb4 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -54,16 +54,13 @@ 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_val ref_clone
-              (fn (fun '(α, β) => FP (λ ϝ, [ϝ ⊑ α; α ⊑ β]%EL)
-                                     [# &shr{α}(ref β ty)]%T (ref β ty)%T)).
+  Lemma ref_clone_type ty `{!TyWf ty} :
+    typed_val ref_clone (fn (fun '(α, β) =>
+                FP_wf ∅ [# &shr{α}(ref β ty)]%T (ref β ty)%T)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
-
-Typeclasses Opaque llctx_interp.
     iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
@@ -119,10 +116,9 @@ Typeclasses Opaque llctx_interp.
       letalloc: "r" <- "r'" in
       delete [ #1; "x"];; return: ["r"].
 
-  Lemma ref_deref_type ty :
+  Lemma ref_deref_type ty `{!TyWf ty} :
     typed_val ref_deref
-      (fn (fun '(α, β) => FP (λ ϝ, [ϝ ⊑ α; α ⊑ β]%EL)
-                             [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T)).
+      (fn (fun '(α, β) => FP_wf ∅ [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -136,12 +132,12 @@ Typeclasses Opaque llctx_interp.
     rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
     iMod "H↦" as "[H↦1 H↦2]". wp_read. wp_let.
     iMod ("Hcloseα" with "[$H↦1 $H↦2]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
     iApply (type_type _ _ _
         [ x ◁ box (&shr{α} ref β ty); #lv ◁ &shr{α}ty]%TC
         with "[] LFT HE Hna HL Hk"); first last.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      iFrame. iApply (ty_shr_mono with "[] Hshr"). iApply lft_incl_glb; last done.
-      rewrite /elctx_interp. iDestruct "HE" as "(_ & $ & _)". }
+      iFrame. iApply (ty_shr_mono with "[] Hshr"). by iApply lft_incl_glb. }
     iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -157,8 +153,8 @@ Typeclasses Opaque llctx_interp.
       delete [ #2; "x"];;
       let: "r" := new [ #0] in return: ["r"].
 
-  Lemma ref_drop_type ty :
-    typed_val ref_drop (fn(∀ α, (λ ϝ, [ϝ ⊑ α]); ref α ty) → unit).
+  Lemma ref_drop_type ty `{!TyWf ty} :
+    typed_val ref_drop (fn(∀ α, ∅; ref α ty) → unit).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -210,67 +206,73 @@ Typeclasses Opaque llctx_interp.
   (* Apply a function within the ref, typically for accessing a component. *)
   Definition ref_map : val :=
     funrec: <> ["ref"; "f"; "env"] :=
-    withcont: "k":
-      let: "x'" := !"ref" in
       let: "f'" := !"f" in
+      Newlft;;
+      let: "x'" := !"ref" in
       letalloc: "x" <- "x'" in
       letcall: "r" := "f'" ["env"; "x"]%E in
-      let: "r'" := !"r" in
+      let: "r'" := !"r" in delete [ #1; "r"];;
+      Endlft;;
       "ref" <- "r'";;
-      delete [ #1; "f"];; "k" []
-    cont: "k" [] :=
-      return: ["ref"].
+      delete [ #1; "f"];; return: ["ref"].
 
-  Lemma ref_map_type ty1 ty2 envty E :
+  Lemma ref_map_type ty1 ty2 envty `{!TyWf ty1, !TyWf ty2, !TyWf envty} :
     typed_val ref_map
-      (fn(∀ β, [β]%EL ++ E;
-            ref β ty1, fn(∀ α, [α]%EL ++ E; envty, &shr{α}ty1) → &shr{α}ty2, envty)
+      (fn(∀ β, ∅; ref β ty1, fn(∀ α, ∅; envty, &shr{α}ty1) → &shr{α}ty2, envty)
        → ref β ty2).
   Proof.
-    intros. 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.
-    iDestruct "HT" as "(Href & Hf & Henv)".
-    destruct ref as [[|lref|]|]; try done. iDestruct "Href" as "[Href Href†]".
+    iApply type_deref; [solve_typing..|]. iIntros (f'). simpl_subst.
+    iApply (type_newlft [ϝ]). iIntros (κ tid) "#LFT #HE Hna HL Hk (Hf & #Hf' & Href & Henv)".
+    rewrite (tctx_hasty_val _ ref). destruct ref as [[|lref|]|]; try done.
+    iDestruct "Href" as "[Href Href†]".
     iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href";
       try iDestruct "Href" as "[_ >[]]".
     rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
     iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
     iDestruct "Href" as (ν qν γ β ty') "(#Hshr & #Hαβ & #Hinv & >Hν & Hγ)".
-    rewrite -(freeable_sz_split _ 1 1). iDestruct "Href†" as "[Href†1 Href†2]".
-    destruct (Qp_lower_bound qE qν) as (q & qE' & qν' & -> & ->).
-    iDestruct (@fractional_split with "HE") as "[[Hα HE] HE']".
-    iDestruct "Hν" as "[Hν Hν']".
-    remember (RecV "k" [] (ret [ LitV lref])%E)%V as k eqn:EQk.
-    iApply (wp_let' _ _ _ _ k). { subst. solve_to_val. } simpl_subst.
-    iApply (type_type ((α ⊓ ν) :: E)%EL []
-        [k ◁cont([], λ _:vec val 0, [ #lref ◁ own_ptr 2 (&shr{α ⊓ ν}ty2)])]%CC
-        [ f ◁ box (fn(∀ α, [α]%EL ++ E; envty, &shr{α}ty1) → &shr{α}ty2);
-          #lref ◁ own_ptr 2 (&shr{α ⊓ ν}ty1); env ◁ box envty ]%TC
-       with "[] LFT Hna [$HE Hα Hν] HL [Hk HE' Hν' Href↦2 Hγ Href†2]"); first last.
-    { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-      iFrame. iApply tctx_hasty_val'. done. iFrame. iExists [_].
-      rewrite heap_mapsto_vec_singleton. by iFrame. }
-    { rewrite !cctx_interp_singleton /=. iIntros "HE". iIntros (args) "Hna HL HT".
-      inv_vec args. subst. simpl. wp_rec. iDestruct "HE" as "[Hαν HE]".
-      iDestruct (lft_tok_sep with "Hαν") as "[Hα Hν]".
-      iSpecialize ("Hk" with "[$HE' $Hα $HE]").
-      iApply ("Hk" $! [# #lref] with "Hna HL").
-      rewrite !tctx_interp_singleton !tctx_hasty_val' //.
-      iDestruct "HT" as "[Href Ḥref†2]".
-      rewrite /= -(freeable_sz_split _ 1 1). iFrame.
-      iDestruct "Href" as ([|[[|lv'|]|] [|]]) "[H↦ Href]"; auto.
-      iExists [ #lv'; #lrc].
-      rewrite (heap_mapsto_vec_cons _ _ _ [_]) !heap_mapsto_vec_singleton. iFrame.
-      iExists ν, (q+qν')%Qp. eauto 10 with iFrame. }
-    { rewrite /= -lft_tok_sep. iFrame. }
-    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
-    iApply type_deref; [solve_typing..|]. 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..|]. iIntros (r'). simpl_subst.
-    iApply type_assign; [solve_typing..|].
+    wp_read. wp_let. wp_apply wp_new; first done.
+    iIntros (lx [|? []]) "(% & H† & Hlx)"; try (simpl in *; lia).
+    rewrite heap_mapsto_vec_singleton. wp_let. wp_write.
+    match goal with | |- context [(WP (_ [?k']) {{_, _}})%I] =>
+      assert (∃ k, to_val k' = Some k) as [k EQk] by (eexists; solve_to_val) end.
+    iApply (wp_let' _ _ _ _ k _ EQk). simpl_subst. iNext.
+    iDestruct (lctx_lft_incl_incl κ α with "HL HE") as "#Hκα"; [solve_typing..|].
+    iMod (bor_create _ κ (qν).[ν] with "LFT [$Hν]") as "[Hb Hν]"; first done.
+    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 _
+        [k ◁cont(_, λ x:vec val 1, [ x!!!0 ◁ box (&shr{α ⊓ ν}ty2)])]%CC
+        [ f' ◁ fn(∀ α, ∅; envty, &shr{α}ty1) → &shr{α}ty2;
+          #lx ◁ box (&shr{α ⊓ ν}ty1); env ◁ box envty ]%TC
+       with "[] LFT [] Hna HL [-H† Hlx Henv]"); swap 1 2; swap 3 4.
+    { iSplitL; last iSplitL; [done|iApply lft_intersect_incl_l|iApply "HE"]. }
+    { iApply (type_call (α ⊓ ν)); solve_typing. }
+    { iFrame "∗#". iApply tctx_hasty_val'; first done. rewrite -freeable_sz_full.
+      iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. auto. }
+    iIntros (? ->%elem_of_list_singleton arg) "Hna HL Hr". inv_vec arg=>r.
+    apply of_to_val in EQk. rewrite EQk. iApply wp_rec; try (done || apply _).
+    { repeat econstructor. by rewrite to_of_val. } simpl_subst.
+    rewrite /tctx_interp big_sepL_singleton (tctx_hasty_val _ r) ownptr_own.
+    iDestruct "Hr" as (lr vr) "(% & Hlr & Hvr & H†)". subst. inv_vec vr=>r'. iNext.
+    rewrite heap_mapsto_vec_singleton. wp_read. wp_let.
+    wp_apply (wp_delete _ _ _ [_] with "[Hlr H†]"). done.
+    { rewrite heap_mapsto_vec_singleton freeable_sz_full. iFrame. }
+    iIntros "_". wp_seq. wp_bind Endlft. iDestruct "HL" as "[Hκ HL]".
+    iDestruct "Hκ" as (κ') "(% & Hκ' & #Hκ'†)". simpl in *. subst κ.
+    iSpecialize ("Hκ'†" with "Hκ'").
+    iApply wp_mask_mono; last iApply (wp_step_fupd with "Hκ'†"); auto with ndisj.
+    wp_seq. iIntros "Hκ'† !>". iMod ("Hν" with "[Hκ'†]") as "Hν";
+      first by rewrite -lft_dead_or; auto. wp_seq. wp_write.
+    iApply (type_type _ _ _
+        [ f ◁ box (fn(∀ α, ∅; envty, &shr{α}ty1) → &shr{α}ty2);
+          #lref ◁ box (ref α ty2) ]%TC
+       with "[] LFT HE Hna HL Hk"); first last.
+    { iFrame. rewrite big_sepL_singleton tctx_hasty_val. iExists _. iSplit. done.
+      iFrame. iExists [_;_]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+      iFrame. destruct r' as [[]|]=>//=. auto 10 with iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 4bfb076b4d1b49297be76baa78805bca356b009a..f34f6305b309983871d49fd916a7307be9773522 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -156,6 +156,9 @@ Section refcell.
     iExists _, _. iFrame. iApply lft_incl_trans; auto.
   Qed.
 
+  Global Instance refcell_wf ty `{!TyWf ty} : TyWf (refcell ty) :=
+    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
   Global Instance refcell_type_ne : TypeNonExpansive refcell.
   Proof.
     constructor;
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index eb8c30909b5048767ac7fdbf31923eeb9f08771b..6f98642452ef6bef6faad1c71f124c575c1b4aad 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -19,8 +19,8 @@ Section refcell_functions.
       "r" +â‚— #1 <-{ty.(ty_size)} !"x";;
       delete [ #ty.(ty_size) ; "x"];; return: ["r"].
 
-  Lemma refcell_new_type ty :
-    typed_val (refcell_new ty) (fn(λ ϝ, []; ty) → refcell ty).
+  Lemma refcell_new_type ty `{!TyWf ty} :
+    typed_val (refcell_new ty) (fn(∅; ty) → refcell ty).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -54,8 +54,8 @@ Section refcell_functions.
              Leaving them away is inconsistent with `let ... := !"x" +â‚— #1`. *)
        delete [ #(S ty.(ty_size)) ; "x"];; return: ["r"].
 
-  Lemma refcell_into_inner_type ty :
-    typed_val (refcell_into_inner ty) (fn(λ ϝ, []; refcell ty) → ty).
+  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 "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -88,9 +88,9 @@ Section refcell_functions.
       "x" <- "x'" +â‚— #1;;
       return: ["x"].
 
-  Lemma refcell_get_mut_type ty :
+  Lemma refcell_get_mut_type ty `{!TyWf ty} :
     typed_val refcell_get_mut
-             (fn(∀ α, λ ϝ, [ϝ ⊑ α]; &uniq{α} (refcell ty)) → &uniq{α} ty)%T.
+              (fn(∀ α, ∅; &uniq{α} (refcell ty)) → &uniq{α} ty)%T.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -139,9 +139,9 @@ Section refcell_functions.
     cont: "k" [] :=
       delete [ #1; "x"];; return: ["r"].
 
-  Lemma refcell_try_borrow_type ty :
+  Lemma refcell_try_borrow_type ty `{!TyWf ty} :
     typed_val refcell_try_borrow
-      (fn(∀ α, λ ϝ, [ϝ ⊑ α] ; &shr{α}(refcell ty)) → option (ref α ty)).
+      (fn(∀ α, ∅; &shr{α}(refcell ty)) → option (ref α ty)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -246,9 +246,9 @@ Section refcell_functions.
     cont: "k" [] :=
       delete [ #1; "x"];; return: ["r"].
 
-  Lemma refcell_try_borrow_mut_type ty :
+  Lemma refcell_try_borrow_mut_type ty `{!TyWf ty} :
     typed_val refcell_try_borrow_mut
-              (fn(∀ α, λ ϝ, [ϝ ⊑ α]; &shr{α}(refcell ty)) → option (refmut α ty))%T.
+              (fn(∀ α, ∅; &shr{α}(refcell ty)) → option (refmut α ty))%T.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 7f12fb47ff22d4026e8f0e9291d046fb0c743d27..98a2abe3304fcd4e7f1608725f3fd3a456d88616 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -72,6 +72,9 @@ Section refmut.
       iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
   Qed.
 
+  Global Instance refmut_wf α ty `{!TyWf ty} : TyWf (refmut α ty) :=
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+
   Global Instance refmut_type_contractive α : TypeContractive (refmut α).
   Proof. solve_type_proper. Qed.
   Global Instance refmut_ne α : NonExpansive (refmut α).
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index af9e25bed470a78bf6bec7126b84abbd50225300..e2649e7c48431684d5a34e7f503711f5d0af1207 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -18,10 +18,9 @@ Section refmut_functions.
       letalloc: "r" <- "r'" in
       delete [ #1; "x"];; return: ["r"].
 
-  Lemma refmut_deref_type ty :
-    typed_val refmut_deref
-      (fn (fun '(α, β) => FP (λ ϝ, [ϝ ⊑ α; α ⊑ β]%EL)
-                             [# &shr{α}(refmut β ty)]%T (&shr{α}ty))).
+  Lemma refmut_deref_type ty `{!TyWf ty} :
+    typed_val refmut_deref (fn (fun '(α, β) =>
+       FP_wf ∅ [# &shr{α}(refmut β ty)]%T (&shr{α}ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -43,11 +42,12 @@ Section refmut_functions.
     iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
     iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1".
     iMod ("Hclose''" with "Hβ HL") as "HL". iMod ("Hclose'" with "[$] HL") as "HL".
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} refmut β ty); #lv ◁ &shr{α}ty]%TC
             with "[] LFT HE Hna HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (ty_shr_mono with "[] Hshr'").
-      iApply lft_incl_glb; last iApply lft_incl_refl. iDestruct "HE" as "(_ & $ & _)". }
+      by iApply lft_incl_glb; last iApply lft_incl_refl. }
     iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -61,10 +61,9 @@ Section refmut_functions.
       letalloc: "r" <- "r'" in
       delete [ #1; "x"];; return: ["r"].
 
-  Lemma refmut_derefmut_type ty :
-    typed_val refmut_derefmut
-      (fn (fun '(α, β) => FP (λ ϝ, [ϝ ⊑ α; α ⊑ β]%EL) [# &uniq{α}(refmut β ty)]%T
-                              (&uniq{α}ty)%T)).
+  Lemma refmut_derefmut_type ty `{!TyWf ty} :
+    typed_val refmut_derefmut (fn (fun '(α, β) =>
+      FP_wf ∅ [# &uniq{α}(refmut β ty)]%T (&uniq{α}ty)%T)).
    Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -96,12 +95,12 @@ Section refmut_functions.
       [done| |by iApply (bor_unnest with "LFT Hb")|]; first done.
     wp_read. iIntros "Hb !>". wp_let.
     iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]". iMod ("Hclose'" with "Hα HL") as "HL".
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
     iApply (type_type _ _ _ [ x ◁ box (uninit 1); #lv ◁ &uniq{α}ty]%TC
             with "[] LFT HE Hna HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (bor_shorten with "[] Hb").
-      iApply lft_incl_glb; [iApply lft_incl_glb|iApply lft_incl_refl]; last done.
-      iDestruct "HE" as "(_ & $ & _)". }
+      by iApply lft_incl_glb; [iApply lft_incl_glb|iApply lft_incl_refl]. }
     iApply (type_letalloc_1 (&uniq{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -116,8 +115,8 @@ Section refmut_functions.
       delete [ #2; "x"];;
       let: "r" := new [ #0] in return: ["r"].
 
-  Lemma refmut_drop_type ty :
-    typed_val refmut_drop (fn(∀ α, (λ ϝ, [ϝ ⊑ α]); refmut α ty) → unit).
+  Lemma refmut_drop_type ty `{!TyWf ty} :
+    typed_val refmut_drop (fn(∀ α, ∅; refmut α ty) → unit).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -159,69 +158,74 @@ Section refmut_functions.
   (* Apply a function within the refmut, typically for accessing a component. *)
   Definition refmut_map : val :=
     funrec: <> ["ref"; "f"; "env"] :=
-    withcont: "k":
-      let: "x'" := !"ref" in
       let: "f'" := !"f" in
+      Newlft;;
+      let: "x'" := !"ref" in
       letalloc: "x" <- "x'" in
       letcall: "r" := "f'" ["env"; "x"]%E in
-      let: "r'" := !"r" in
+      let: "r'" := !"r" in delete [ #1; "r"];;
+      Endlft;;
       "ref" <- "r'";;
-      delete [ #1; "f"];; "k" []
-    cont: "k" [] :=
-      return: ["ref"].
+      delete [ #1; "f"];; return: ["ref"].
 
-  Lemma refmut_map_type ty1 ty2 envty E :
+  Lemma refmut_map_type ty1 ty2 envty `{!TyWf ty1, !TyWf ty2, !TyWf envty} :
     typed_val refmut_map
-      (fn(∀ β, [β]%EL ++ E; refmut β ty1,
-                         fn(∀ α, [α]%EL ++ E; envty, &uniq{α} ty1) → &uniq{α} ty2,
-                         envty)
+      (fn(∀ β, ∅; refmut β ty1,
+            fn(∀ α, ∅; envty, &uniq{α} ty1) → &uniq{α} ty2, envty)
        → refmut β ty2).
   Proof.
-    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)".
-    destruct ref as [[|lref|]|]; try done. iDestruct "Href" as "[Href Href†]".
+    intros. 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)".
+    rewrite (tctx_hasty_val _ ref). destruct ref as [[|lref|]|]; try done.
+    iDestruct "Href" as "[Href Href†]".
     iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href";
       try iDestruct "Href" as "[_ >[]]".
     rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
     iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
     iDestruct "Href" as (ν γ β ty') "(Hbor & #Hαβ & #Hinv & >Hν & Hγ)".
-    rewrite -(freeable_sz_split _ 1 1). iDestruct "Href†" as "[Href†1 Href†2]".
-    destruct (Qp_lower_bound qE 1) as (q & qE' & qν' & -> & EQ1).
-      rewrite [in (_).[ν]%I] EQ1.
-    iDestruct (@fractional_split with "HE") as "[[Hα HE] HE']".
-    iDestruct "Hν" as "[Hν Hν']".
-    remember (RecV "k" [] (ret [ LitV lref])%E)%V as k eqn:EQk.
-    iApply (wp_let' _ _ _ _ k). { subst. solve_to_val. } simpl_subst.
-    iApply (type_type ((α ⊓ ν) :: E)%EL []
-        [k ◁cont([], λ _:vec val 0, [ #lref ◁ own_ptr 2 (&uniq{α ⊓ ν}ty2)])]%CC
-        [ f ◁ box (fn(∀ α, [α]%EL ++ E; envty, &uniq{α}ty1) → &uniq{α}ty2);
-          #lref ◁ own_ptr 2 (&uniq{α ⊓ ν}ty1); env ◁ box envty ]%TC
-       with "[] LFT Hna [$HE Hα Hν] HL [Hk HE' Hν' Href↦2 Hγ Href†2]"); first last.
-    { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-      iFrame. iApply tctx_hasty_val'. done. iFrame. iExists [_].
-      rewrite heap_mapsto_vec_singleton. by iFrame. }
-    { rewrite !cctx_interp_singleton /=. iIntros "HE". iIntros (args) "Hna HL HT".
-      inv_vec args. subst. simpl. wp_rec. iDestruct "HE" as "[Hαν HE]".
-      iDestruct (lft_tok_sep with "Hαν") as "[Hα Hν]".
-      iSpecialize ("Hk" with "[$HE' $Hα $HE]").
-      iApply ("Hk" $! [# #lref] with "Hna HL").
-      rewrite !tctx_interp_singleton !tctx_hasty_val' //.
-      iDestruct "HT" as "[Href Ḥref†2]".
-      rewrite /= -(freeable_sz_split _ 1 1). iFrame.
-      iDestruct "Href" as ([|[[|lv'|]|] [|]]) "[H↦ Href]"; auto.
-      iExists [ #lv'; #lrc].
-      rewrite (heap_mapsto_vec_cons _ _ _ [_]) !heap_mapsto_vec_singleton. iFrame.
-      iExists ν. rewrite /= EQ1. eauto 20 with iFrame. }
-    { rewrite /= -lft_tok_sep. iFrame. }
-    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
-    iApply type_deref; [solve_typing..|]. 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..|]. iIntros (r'). simpl_subst.
-    iApply type_assign; [solve_typing..|].
+    wp_read. wp_let. wp_apply wp_new; first done.
+    iIntros (lx [|? []]) "(% & H† & Hlx)"; try (simpl in *; lia).
+    rewrite heap_mapsto_vec_singleton. wp_let. wp_write.
+    match goal with | |- context [(WP (_ [?k']) {{_, _}})%I] =>
+      assert (∃ k, to_val k' = Some k) as [k EQk] by (eexists; solve_to_val) end.
+    iApply (wp_let' _ _ _ _ k _ EQk). simpl_subst. iNext.
+    iDestruct (lctx_lft_incl_incl κ α with "HL HE") as "#Hκα"; [solve_typing..|].
+    iMod (bor_create _ κ (1).[ν] with "LFT [$Hν]") as "[Hb Hν]"; first done.
+    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 _
+        [k ◁cont(_, λ x:vec val 1, [ x!!!0 ◁ box (&uniq{α ⊓ ν}ty2)])]%CC
+        [ f' ◁ fn(∀ α, ∅; envty, &uniq{α}ty1) → &uniq{α}ty2;
+          #lx ◁ box (&uniq{α ⊓ ν}ty1); env ◁ box envty ]%TC
+       with "[] LFT [] Hna HL [-H† Hlx Henv Hbor]"); swap 1 2; swap 3 4.
+    { iSplitL; last iSplitL; [done|iApply lft_intersect_incl_l|iApply "HE"]. }
+    { iApply (type_call (α ⊓ ν)); solve_typing. }
+    { iFrame "∗#". iApply tctx_hasty_val'; first done. rewrite -freeable_sz_full.
+      iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. auto with iFrame. }
+    iIntros (? ->%elem_of_list_singleton arg) "Hna HL Hr". inv_vec arg=>r.
+    apply of_to_val in EQk. rewrite EQk. iApply wp_rec; try (done || apply _).
+    { repeat econstructor. by rewrite to_of_val. } simpl_subst.
+    rewrite /tctx_interp big_sepL_singleton (tctx_hasty_val _ r) ownptr_own.
+    iDestruct "Hr" as (lr vr) "(% & Hlr & Hvr & H†)". subst. inv_vec vr=>r'. iNext.
+    rewrite heap_mapsto_vec_singleton. wp_read. wp_let.
+    wp_apply (wp_delete _ _ _ [_] with "[Hlr H†]"). done.
+    { rewrite heap_mapsto_vec_singleton freeable_sz_full. iFrame. }
+    iIntros "_". wp_seq. wp_bind Endlft. iDestruct "HL" as "[Hκ HL]".
+    iDestruct "Hκ" as (κ') "(% & Hκ' & #Hκ'†)". simpl in *. subst κ.
+    iSpecialize ("Hκ'†" with "Hκ'").
+    iApply wp_mask_mono; last iApply (wp_step_fupd with "Hκ'†"); auto with ndisj.
+    wp_seq. iIntros "Hκ'† !>". iMod ("Hν" with "[Hκ'†]") as "Hν";
+      first by rewrite -lft_dead_or; auto. wp_seq. wp_write.
+    iApply (type_type _ _ _
+        [ f ◁ box (fn(∀ α, ∅; envty, &uniq{α}ty1) → &uniq{α}ty2);
+          #lref ◁ box (refmut α ty2) ]%TC
+       with "[] LFT HE Hna HL Hk"); first last.
+    { iFrame. rewrite big_sepL_singleton tctx_hasty_val. iExists _. iSplit. done.
+      iFrame. iExists [_;_]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+      iFrame. destruct r' as [[]|]=>//=. auto 10 with iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index fe5b772d78f3298c20df8e316ad44baefa6bc2f1..db17b3e5830be1ea7c2944aa7cf6055eda0c95d5 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -149,6 +149,9 @@ Section rwlock.
     iExists _, _. iFrame. iApply lft_incl_trans; auto.
   Qed.
 
+  Global Instance join_handle_wf ty `{!TyWf ty} : TyWf (rwlock ty) :=
+    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
   Global Instance rwlock_type_ne : TypeNonExpansive rwlock.
   Proof.
     constructor;
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 408778d961dc465402d8b344cf0dc80407125b2b..1298abb58690d0cee78da37db4dd90009127f242 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -19,8 +19,8 @@ Section rwlock_functions.
       "r" +â‚— #1 <-{ty.(ty_size)} !"x";;
        delete [ #ty.(ty_size) ; "x"];; return: ["r"].
 
-  Lemma rwlock_new_type ty :
-    typed_val (rwlock_new ty) (fn(λ ϝ, []; ty) → rwlock ty).
+  Lemma rwlock_new_type ty `{!TyWf ty} :
+    typed_val (rwlock_new ty) (fn(∅; ty) → rwlock ty).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ret ϝ arg). inv_vec arg=>x. simpl_subst.
@@ -55,8 +55,8 @@ Section rwlock_functions.
       "r" <-{ty.(ty_size)} !("x" +â‚— #1);;
        delete [ #(S ty.(ty_size)) ; "x"];; return: ["r"].
 
-  Lemma rwlock_into_inner_type ty :
-    typed_val (rwlock_into_inner ty) (fn(λ ϝ, [] ; rwlock ty) → ty).
+  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 "/= !#".
       iIntros (_ ret ϝ arg). inv_vec arg=>x. simpl_subst.
@@ -89,8 +89,8 @@ Section rwlock_functions.
       "x" <- "x'" +â‚— #1;;
       return: ["x"].
 
-  Lemma rwlock_get_mut_type ty :
-    typed_val rwlock_get_mut (fn(∀ α, λ ϝ, [ϝ ⊑ α]; &uniq{α} (rwlock ty)) → &uniq{α} ty).
+  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 "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -139,9 +139,9 @@ Section rwlock_functions.
     cont: "k" [] :=
       delete [ #1; "x"];; return: ["r"].
 
-  Lemma rwlock_try_read_type ty :
+  Lemma rwlock_try_read_type ty `{!TyWf ty} :
     typed_val rwlock_try_read
-        (fn(∀ α, λ ϝ, [ϝ ⊑ α]; &shr{α}(rwlock ty)) → option (rwlockreadguard α ty)).
+        (fn(∀ α, ∅; &shr{α}(rwlock ty)) → option (rwlockreadguard α ty)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -254,9 +254,9 @@ Section rwlock_functions.
     cont: "k" ["r"] :=
       delete [ #1; "x"];; return: ["r"].
 
-  Lemma rwlock_try_write_type ty :
+  Lemma rwlock_try_write_type ty `{!TyWf ty} :
     typed_val rwlock_try_write
-        (fn(∀ α, λ ϝ, [ϝ ⊑ α]; &shr{α}(rwlock ty)) → option (rwlockwriteguard α ty)).
+        (fn(∀ α, ∅; &shr{α}(rwlock ty)) → option (rwlockwriteguard α ty)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index e023b7a3515552e5c8c6da60486a167a2b07abbf..3f44a88e8d599be379c2eae4b57633218ad58169 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -61,6 +61,9 @@ Section rwlockreadguard.
     iApply lft_incl_refl.
   Qed.
 
+  Global Instance rwlockreadguard_wf α ty `{!TyWf ty} : TyWf (rwlockreadguard α ty) :=
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+
   Global Instance rwlockreadguard_type_contractive α : TypeContractive (rwlockreadguard α).
   Proof.
     constructor;
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 4fb1418b380fcc6216ed3b6a2a1c6e16b6f4b70c..e53896fcc304360e0cc85467fabea7d22c4903b9 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -18,10 +18,9 @@ Section rwlockreadguard_functions.
       letalloc: "r" <- "r'" in
       delete [ #1; "x"];; return: ["r"].
 
-  Lemma rwlockreadguard_deref_type ty :
+  Lemma rwlockreadguard_deref_type ty `{!TyWf ty} :
     typed_val rwlockreadguard_deref
-      (fn (fun '(α, β) => FP (λ ϝ, [ϝ ⊑ α; α ⊑ β]%EL)
-                             [# &shr{α}(rwlockreadguard β ty)] (&shr{α}ty))).
+      (fn (fun '(α, β) => FP_wf ∅ [# &shr{α}(rwlockreadguard β ty)] (&shr{α}ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -34,12 +33,13 @@ Section rwlockreadguard_functions.
     iMod (frac_bor_acc with "LFT Hfrac Hα") as (qlx') "[H↦ Hcloseα]". done.
     rewrite heap_mapsto_vec_singleton. wp_read. wp_op. wp_let.
     iMod ("Hcloseα" with "[$H↦]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} rwlockreadguard β ty);
                               #(shift_loc l' 1) ◁ &shr{α}ty]%TC
       with "[] LFT HE Hna HL Hk"); first last.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      iFrame. iApply (ty_shr_mono with "[] Hshr"). iApply lft_incl_glb.
-      by iDestruct "HE" as "(_ & $ & _)". by iApply lft_incl_refl. }
+      iFrame. iApply (ty_shr_mono with "[] Hshr"). iApply lft_incl_glb; first done.
+      by iApply lft_incl_refl. }
     iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -58,9 +58,8 @@ Section rwlockreadguard_functions.
         let: "r" := new [ #0] in return: ["r"]
       else "loop" [].
 
-  Lemma rwlockreadguard_drop_type ty :
-    typed_val rwlockreadguard_drop
-              (fn(∀ α, λ ϝ, [ϝ ⊑ α]; rwlockreadguard α ty) → unit).
+  Lemma rwlockreadguard_drop_type ty `{!TyWf ty} :
+    typed_val rwlockreadguard_drop (fn(∀ α, ∅; rwlockreadguard α ty) → unit).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index b71f6c763fb6bb7a9f0683567dedfa4d4cf16af2..7003099dff1d60b3a7d5dc2842d6706f5bb52a11 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -61,6 +61,9 @@ Section rwlockwriteguard.
       iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
   Qed.
 
+  Global Instance rwlockwriteguard_wf α ty `{!TyWf ty} : TyWf (rwlockwriteguard α ty) :=
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+
   Global Instance rwlockwriteguard_type_contractive α : TypeContractive (rwlockwriteguard α).
   Proof.
     constructor;
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index ba11a3a3b02cca2030029fd36efb7a52b304fa55..7ccd5321e11c58d0e4a57a66caae4b64a2c2e5d7 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -18,10 +18,9 @@ Section rwlockwriteguard_functions.
       letalloc: "r" <- "r'" in
       delete [ #1; "x"];; return: ["r"].
 
-  Lemma rwlockwriteguard_deref_type ty :
+  Lemma rwlockwriteguard_deref_type ty `{!TyWf ty} :
     typed_val rwlockwriteguard_deref
-      (fn (fun '(α, β) => FP (λ ϝ, [ϝ ⊑ α; α ⊑ β]%EL)
-                             [# &shr{α}(rwlockwriteguard β ty)] (&shr{α}ty))).
+      (fn (fun '(α, β) => FP_wf ∅ [# &shr{α}(rwlockwriteguard β ty)] (&shr{α}ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -43,12 +42,13 @@ Section rwlockwriteguard_functions.
     iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
     iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1". iMod ("Hclose'" with "Hβ HL") as "HL".
     iMod ("Hclose" with "[$] HL") as "HL".
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} rwlockwriteguard β ty);
                               #(shift_loc l' 1) ◁ &shr{α}ty]%TC
             with "[] LFT HE Hna HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      iFrame. iApply (ty_shr_mono with "[] Hshr'"). iApply lft_incl_glb.
-        by iDestruct "HE" as "(_ & $ & _)". by iApply lft_incl_refl. }
+      iFrame. iApply (ty_shr_mono with "[] Hshr'"). iApply lft_incl_glb; first done.
+        by iApply lft_incl_refl. }
     iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -62,10 +62,9 @@ Section rwlockwriteguard_functions.
       letalloc: "r" <- "r'" in
       delete [ #1; "x"];; return: ["r"].
 
-  Lemma rwlockwriteguard_derefmut_type ty :
+  Lemma rwlockwriteguard_derefmut_type ty `{!TyWf ty} :
     typed_val rwlockwriteguard_derefmut
-      (fn (fun '(α, β) => FP (λ ϝ, [ϝ ⊑ α; α ⊑ β]%EL)
-                             [# &uniq{α}(rwlockwriteguard β ty)] (&uniq{α}ty))).
+      (fn (fun '(α, β) => FP_wf ∅ [# &uniq{α}(rwlockwriteguard β ty)] (&uniq{α}ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -89,12 +88,12 @@ Section rwlockwriteguard_functions.
       [done| |by iApply (bor_unnest with "LFT Hb")|]; first done.
     wp_read. iIntros "Hb !>". wp_op. wp_let.
     iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]". iMod ("Hclose" with "Hα HL") as "HL".
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
     iApply (type_type _ _ _ [ x ◁ box (uninit 1); #(shift_loc l 1) ◁ &uniq{α}ty]%TC
             with "[] LFT HE Hna HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (bor_shorten with "[] Hb"). iApply lft_incl_glb.
-      by iApply lft_incl_trans; first iDestruct "HE" as "(_ & $ & _)".
-      by iApply lft_incl_refl. }
+      by iApply lft_incl_trans. by iApply lft_incl_refl. }
     iApply (type_letalloc_1 (&uniq{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -108,9 +107,9 @@ Section rwlockwriteguard_functions.
       delete [ #1; "x"];;
       let: "r" := new [ #0] in return: ["r"].
 
-  Lemma rwlockwriteguard_drop_type ty :
+  Lemma rwlockwriteguard_drop_type ty `{!TyWf ty} :
     typed_val rwlockwriteguard_drop
-              (fn(∀ α, λ ϝ, [ϝ ⊑ α]; rwlockwriteguard α ty) → unit).
+              (fn(∀ α, ∅; rwlockwriteguard α ty) → unit).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -120,7 +119,8 @@ Section rwlockwriteguard_functions.
     iDestruct "HT" as "[Hx Hx']".
     destruct x' as [[|lx'|]|]; try done. simpl.
     iDestruct "Hx'" as (γ β) "(Hx' & #Hαβ & #Hinv & H◯)".
-    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)";
+      [solve_typing..|].
     iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
     wp_bind (#lx' <-ˢᶜ #0)%E.
     iMod (shr_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index fcaa8747f08c19fc3e7f0e6980c2b9b6629e8bc3..d2a67fab880097b13687536aaad9ab54238592c6 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -26,6 +26,9 @@ Section join_handle.
   Next Obligation. iIntros "* _ _ _ $". auto. Qed.
   Next Obligation. iIntros (?) "**"; auto. Qed.
 
+  Global Instance join_handle_wf ty `{!TyWf ty} : TyWf (join_handle ty) :=
+    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
   Lemma join_handle_subtype ty1 ty2 :
     ▷ type_incl ty1 ty2 -∗ type_incl (join_handle ty1) (join_handle ty2).
   Proof.
@@ -67,8 +70,10 @@ Section spawn.
       letalloc: "r" <- "join" in
       delete [ #1; "f"];; return: ["r"].
 
-  Lemma spawn_type `(!Send envty, !Send retty) :
-    typed_val spawn (fn(λ _, []; fn(λ _, [] ; envty) → retty, envty) → join_handle retty).
+  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 "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>f env. simpl_subst.
@@ -84,13 +89,13 @@ Section spawn.
         iIntros "?". iExists retty. iFrame. iApply type_incl_refl. }
       iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let.
       (* FIXME this is horrible. *)
-      assert (Hcall := type_call' [] [] [] f' [] [env:expr] (λ _:(), FP (λ _, []) [# envty] retty)).
+      refine (let Hcall := type_call' _ [] [] f' [] [env:expr]
+                (λ _:(), FP_wf ∅ [# envty] retty) in _).
       specialize (Hcall (rec: "_k" ["r"] := finish [ #c; "r"])%V ()).
       erewrite of_val_unlock in Hcall; last done.
-      iApply (Hcall with "LFT [] Htl [] [Hfin]").
+      iApply (Hcall with "LFT HE Htl [] [Hfin]").
       - constructor.
-      - intros. apply elctx_sat_nil.
-      - rewrite /elctx_interp big_sepL_nil. done.
+      - solve_typing.
       - rewrite /llctx_interp big_sepL_nil. done.
       - rewrite /cctx_interp. iIntros "* Hin".
         iDestruct "Hin" as %Hin%elem_of_list_singleton. subst x.
@@ -98,9 +103,8 @@ Section spawn.
         wp_rec. iApply (finish_spec with "[$Hfin Hret]"); last auto.
         rewrite tctx_interp_singleton tctx_hasty_val. by iApply @send_change_tid.
       - rewrite tctx_interp_cons tctx_interp_singleton. iSplitL "Hf'".
-        + rewrite !tctx_hasty_val.
-          iApply @send_change_tid. done.
-        + rewrite !tctx_hasty_val. iApply @send_change_tid. done. }
+        + rewrite !tctx_hasty_val. by iApply @send_change_tid.
+        + rewrite !tctx_hasty_val. by iApply @send_change_tid. }
     iIntros (v). simpl_subst.
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_assign; [solve_typing..|].
@@ -114,8 +118,8 @@ Section spawn.
       let: "r" := join ["c'"] in
       delete [ #1; "c"];; return: ["r"].
 
-  Lemma join_type retty :
-    typed_val join (fn(λ _, []; join_handle retty) → retty).
+  Lemma join_type retty `{!TyWf retty} :
+    typed_val join (fn(∅; join_handle retty) → retty).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>c. simpl_subst.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 76a252aed2e95c139400990c9d6cca7a3ab8b7e2..1fee0f1222317aff9c295c4ef89583859ca1de1e 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -63,8 +63,8 @@ Section own.
          end%I;
        ty_shr κ tid l :=
          (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
-            □ (∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ] ={F,F∖↑shrN}▷=∗ ty.(ty_shr) κ tid l' ∗ q.[κ]))%I
-    |}.
+            □ (∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ] ={F,F∖↑shrN}▷=∗
+                            ty.(ty_shr) κ tid l' ∗ q.[κ]))%I |}.
   Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed.
   Next Obligation.
     move=>n ty N κ l tid ?? /=. iIntros "#LFT Hshr Htok".
@@ -88,6 +88,9 @@ Section own.
     by iApply (ty.(ty_shr_mono) with "Hκ").
   Qed.
 
+  Global Instance own_ptr_wf n ty `{!TyWf ty} : TyWf (own_ptr n ty) :=
+    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
   Lemma own_type_incl n m ty1 ty2 :
     ▷ ⌜n = m⌝ -∗ ▷ type_incl ty1 ty2 -∗ type_incl (own_ptr n ty1) (own_ptr m ty2).
   Proof.
@@ -186,7 +189,8 @@ Section util.
 
   Lemma ownptr_own n ty tid v :
     (own_ptr n ty).(ty_own) tid [v] ⊣⊢
-       ∃ (l : loc) (vl : vec val ty.(ty_size)), ⌜v = #l⌝ ∗ ▷ l ↦∗ vl ∗ ▷ ty.(ty_own) tid vl ∗ ▷ freeable_sz n ty.(ty_size) l.
+       ∃ (l : loc) (vl : vec val ty.(ty_size)),
+         ⌜v = #l⌝ ∗ ▷ l ↦∗ vl ∗ ▷ ty.(ty_own) tid vl ∗ ▷ freeable_sz n ty.(ty_size) l.
   Proof.
     iSplit.
     - iIntros "Hown". destruct v as [[|l|]|]; try done.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 50c7427b9739edd1aa6832bba2a471b055135e61..a51abc5358006379c1dc9bda92e4c8c9d0e4edc9 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -148,6 +148,9 @@ Section product.
   Definition product := foldr product2 unit0.
   Definition unit := product [].
 
+  Global Instance product_wf tyl `{!TyWfLst tyl} : TyWf (product tyl) :=
+    { ty_lfts := tyl.(tyl_lfts); ty_wf_E := tyl.(tyl_wf_E) }.
+
   Global Instance product_type_ne n: Proper (Forall2 (type_dist2 n) ==> type_dist2 n) product.
   Proof. intros ??. induction 1=>//=. by f_equiv. Qed.
   Global Instance product_ne : NonExpansive product.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 311dad58a263e177eff994552d6976ec156c4f9d..a7cad9b8270abd495b23d11cae3809b9d2d945e6 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -16,6 +16,9 @@ Section shr_bor.
   Next Obligation. by iIntros (κ ty tid [|[[]|][]]) "H". Qed.
   Next Obligation. intros κ ty tid [|[[]|][]]; apply _. Qed.
 
+  Global Instance shr_bor_wf κ ty `{!TyWf ty} : TyWf (shr_bor κ ty) :=
+    { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) κ }.
+
   Global Instance shr_mono E L :
     Proper (flip (lctx_lft_incl E L) ==> subtype E L ==> subtype E L) shr_bor.
   Proof.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 38166586412c8f21b538b7a8fd4cde46f012e1cc..42ba0dbbbb99af88b59b4ac1f5b0bcf5c72a705a 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -23,7 +23,7 @@ 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_val main main_type) →
@@ -53,7 +53,7 @@ Section type_soundness.
     iMod (lft_create with "LFT") as (ϝ) "Hϝ". done.
     iApply ("Hmain" $! () ϝ exit_cont [#] tid with "LFT [] Htl [Hϝ] []");
       last by rewrite tctx_interp_nil.
-    { by rewrite /elctx_interp /=. }
+    { by rewrite /elctx_interp /= big_sepL_nil. }
     { rewrite /llctx_interp big_sepL_singleton. iExists ϝ. iFrame. by rewrite /= left_id. }
     rewrite cctx_interp_singleton. simpl. iIntros (args) "_ _".
     inv_vec args. iIntros (x) "_ /=". by wp_lam.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index e48d0aea8b2441cd7d644855dafad47e27c3e294..450483311d2b6fea979b2e5da38beebea515a2a2 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -20,6 +20,8 @@ Section sum.
   Qed.
   Next Obligation. iIntros (κ κ' tid l) "#Hord []". Qed.
 
+  Global Instance emp_wf : TyWf emp := { ty_lfts := []; ty_wf_E := [] }.
+
   Global Instance emp_empty : Empty type := emp.
 
   Global Instance emp_copy : Copy ∅.
@@ -92,6 +94,9 @@ Section sum.
     - iApply ((nth i tyl ∅).(ty_shr_mono) with "Hord"); done.
   Qed.
 
+  Global Instance sum_wf tyl `{!TyWfLst tyl} : TyWf (sum tyl) :=
+    { ty_lfts := tyl.(tyl_lfts); ty_wf_E := tyl.(tyl_wf_E) }.
+
   Global Instance sum_type_ne n : Proper (Forall2 (type_dist2 n) ==> type_dist2 n) sum.
   Proof.
     intros x y EQ.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index b0ad75fff224e2fc19befeab57ba1a88256c3920..401392ae02e3b6a3ce1bd5938e165ecf789a0e56 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -53,6 +53,61 @@ Instance: Params (@ty_shr) 2.
 
 Arguments ty_own {_ _} _ _ !_ /.
 
+Class TyWf `{typeG Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
+Arguments ty_lfts {_ _} _ {_}.
+Arguments ty_wf_E {_ _} _ {_}.
+
+Definition ty_outlives_E `{typeG Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
+  (λ α, κ ⊑ α)%EL <$> ty.(ty_lfts).
+
+Lemma ty_outlives_E_elctx_sat `{typeG Σ} E L ty `{!TyWf ty} α β :
+  ty.(ty_outlives_E) β ⊆+ E →
+  lctx_lft_incl E L α β →
+  elctx_sat E L (ty.(ty_outlives_E) α).
+Proof.
+  unfold ty_outlives_E. induction ty.(ty_lfts) as [|κ l IH]=>/= Hsub Hαβ.
+  - solve_typing.
+  - apply elctx_sat_lft_incl.
+    + etrans; first done. eapply lctx_lft_incl_external, elem_of_submseteq, Hsub.
+      set_solver.
+    + apply IH, Hαβ. etrans; last done. by apply submseteq_cons.
+Qed.
+
+Inductive TyWfLst `{typeG Σ} : list type → Type :=
+| tyl_wf_nil : TyWfLst []
+| tyl_wf_cons ty tyl `{!TyWf ty, !TyWfLst tyl} : TyWfLst (ty::tyl).
+Existing Class TyWfLst.
+Existing Instances tyl_wf_nil tyl_wf_cons.
+
+Fixpoint tyl_lfts `{typeG Σ} tyl {WF : TyWfLst tyl} : list lft :=
+  match WF with
+  | tyl_wf_nil => []
+  | tyl_wf_cons ty tyl _ _ => ty.(ty_lfts) ++ tyl.(tyl_lfts)
+  end.
+
+Fixpoint tyl_wf_E `{typeG Σ} tyl {WF : TyWfLst tyl} : elctx :=
+  match WF with
+  | tyl_wf_nil => []
+  | tyl_wf_cons ty tyl _ _ => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
+  end.
+
+Fixpoint tyl_outlives_E `{typeG Σ} tyl {WF : TyWfLst tyl} (κ : lft) : elctx :=
+  match WF with
+  | tyl_wf_nil => []
+  | tyl_wf_cons ty tyl _ _ => ty.(ty_outlives_E) κ ++ tyl.(tyl_outlives_E) κ
+  end.
+
+Lemma tyl_outlives_E_elctx_sat `{typeG Σ} E L tyl {WF : TyWfLst tyl} α β :
+  tyl.(tyl_outlives_E) β ⊆+ E →
+  lctx_lft_incl E L α β →
+  elctx_sat E L (tyl.(tyl_outlives_E) α).
+Proof.
+  induction WF as [|???? IH]=>/=.
+  - solve_typing.
+  - intros. apply elctx_sat_app, IH; [eapply ty_outlives_E_elctx_sat| |]=>//;
+      (etrans; [|done]); solve_typing.
+Qed.
+
 Record simple_type `{typeG Σ} :=
   { st_own : thread_id → list val → iProp Σ;
     st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%nat⌝;
@@ -194,8 +249,7 @@ Section ofe.
 
   Global Instance ty_of_st_ne : NonExpansive ty_of_st.
   Proof.
-    intros n ?? EQ. constructor. done. simpl.
-    - intros tid l. apply EQ.
+    intros n ?? EQ. constructor; try apply EQ. done.
     - simpl. intros; repeat f_equiv. apply EQ.
   Qed.
   Global Instance ty_of_st_proper : Proper ((≡) ==> (≡)) ty_of_st.
@@ -515,8 +569,8 @@ Section subtyping.
     iClear "∗". iIntros "!# #HE".
     iApply (type_incl_trans with "[#]"). by iApply "H12". by iApply "H23".
   Qed.
-  
-  Lemma subtype_Forall2_llctx E L tys1 tys2 qL : 
+
+  Lemma subtype_Forall2_llctx E L tys1 tys2 qL :
     Forall2 (subtype E L) tys1 tys2 →
     llctx_interp L qL -∗ □ (elctx_interp E -∗
            [∗ list] tys ∈ (zip tys1 tys2), type_incl (tys.1) (tys.2)).
@@ -584,7 +638,7 @@ Section subtyping.
   Qed.
 
   Lemma subtype_simple_type E L (st1 st2 : simple_type) :
-    (∀ qL, llctx_interp L qL -∗ □ (elctx_interp E -∗ 
+    (∀ qL, llctx_interp L qL -∗ □ (elctx_interp E -∗
        ∀ tid vl, st1.(st_own) tid vl -∗ st2.(st_own) tid vl)) →
     subtype E L st1 st2.
   Proof.
@@ -608,7 +662,7 @@ End subtyping.
 
 Section type_util.
   Context `{typeG Σ}.
-  
+
   Lemma heap_mapsto_ty_own l ty tid :
     l ↦∗: ty_own ty tid ⊣⊢ ∃ (vl : vec val ty.(ty_size)), l ↦∗ vl ∗ ty_own ty tid vl.
   Proof.
@@ -621,5 +675,6 @@ Section type_util.
 
 End type_util.
 
+Hint Resolve ty_outlives_E_elctx_sat tyl_outlives_E_elctx_sat : lrust_typing.
 Hint Resolve subtype_refl eqtype_refl : lrust_typing.
 Hint Opaque subtype eqtype : lrust_typing.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index 294fb3721164eff16ac29a7041e4ed8fb3fa584d..b8852230083a62bfcaeac3e7c47d88c62ecadd6f 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -17,7 +17,7 @@ Section uninit.
     Π (replicate n uninit_1).
 
   Lemma uninit0_sz n : ty_size (uninit0 n) = n.
-  Proof. induction n. done. simpl. by f_equal. Qed.
+  Proof. induction n=>//=. by f_equal. Qed.
 
   (* We redefine uninit as an alias of uninit0, so that the size
      computes directly to [n] *)
@@ -28,6 +28,9 @@ Section uninit.
   Next Obligation. intros. by apply ty_share. Qed.
   Next Obligation. intros. by apply ty_shr_mono. Qed.
 
+  Global Instance uninit_wf n : TyWf (uninit n) :=
+    { ty_lfts := []; ty_wf_E := [] }.
+
   Global Instance uninit_copy n : Copy (uninit n).
   Proof.
     destruct (product_copy (replicate n uninit_1)) as [A B].
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 722c74e2bc88f391a615e77e7de874216a886e14..e8f07a2d160210416c3cef2164ea2b6f826dde12 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -43,6 +43,9 @@ Section uniq_bor.
     by iApply (ty_shr_mono with "Hκ0").
   Qed.
 
+  Global Instance uniq_bor_wf κ ty `{!TyWf ty} : TyWf (uniq_bor κ ty) :=
+    { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) κ }.
+
   Global Instance uniq_mono E L :
     Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) uniq_bor.
   Proof.