diff --git a/README.md b/README.md
index 6d6891023d77c8d8599b5aef6ba80ccacda2cde5..3ace436a0506f36dd33afdae71ca95123de4784f 100644
--- a/README.md
+++ b/README.md
@@ -52,6 +52,26 @@ followed by `make build-dep`.
     `thread::spawn`, `take_mut::take`, `alias::once` as well as converting `&&T`
     to `&Box<T>`.
 
+## Changes since original RustBelt publication
+
+In this section we list fundamental changes to the model that were done since
+the publication of the
+[original RustBelt paper](https://plv.mpi-sws.org/rustbelt/popl18/).
+
+### Support for branding
+
+As part of the [GhostCell paper](http://plv.mpi-sws.org/rustbelt/ghostcell/),
+the model was adjusted to support branding.
+
+* The semantic interpretation of external lifetime contexts had to be changed to use a *syntactic* form of lifetime inclusion.
+* This changed interpretation broke the proof of "lifetime equalization".
+    Instead we prove a weaker rule that only substitutes lifetimes on positions that are compatible with *semantic* lifetime inclusion.
+    This is good enough for [the example](theories/typing/examples/nonlexical.v).
+* Furthermore, we had to redo the proof of `type_call_iris'`, a key lemma involved in calling functions and ensuring that their assumptions about lifetime parameters do indeed hold.
+    The old proof exploited *semantic* lifetime inclusion in external lifetime contexts in a crucial step.
+    The proof was fixed by adjusting the semantic interpretation of the local lifetime context.
+    In particular there is a new parameter `qmax` here that has to be threaded through everywhere.
+
 ## Where to Find the Proof Rules From the Paper
 
 ### Type System Rules
diff --git a/_CoqProject b/_CoqProject
index fbc95688afcf1ab8f7d7da00675952e4d709d429..ceef9efbc4957f1d8ddf730085784a0e52b01de1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -68,6 +68,7 @@ theories/typing/lib/rc/rc.v
 theories/typing/lib/rc/weak.v
 theories/typing/lib/arc.v
 theories/typing/lib/swap.v
+theories/typing/lib/diverging_static.v
 theories/typing/lib/mutex/mutex.v
 theories/typing/lib/mutex/mutexguard.v
 theories/typing/lib/refcell/refcell.v
@@ -88,4 +89,3 @@ theories/typing/examples/unbox.v
 theories/typing/examples/init_prod.v
 theories/typing/examples/lazy_lft.v
 theories/typing/examples/nonlexical.v
-theories/typing/examples/diverging_static.v
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 000abf66f7e241aa228e2cd83101d5f81c54f23e..ca213604ae7f1981de8ab59f64f885b40f904ac7 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -84,7 +84,7 @@ Notation "'withcont:' k1 ':' e1 'cont:' k2 xl := e2" :=
   ((Lam (@cons binder k1%binder nil) e1%E) [Rec k2%binder ((fun _ : eq k1%binder k2%binder => xl%binder) eq_refl) e2%E])
   (only parsing, at level 151, k1, k2, xl at level 1, e2 at level 150) : expr_scope.
 
-Notation "'call:' f args → k" := (f (@cons expr (λ: ["_r"], Endlft ;; k ["_r"]) args))%E
+Notation "'call:' f args → k" := (f (@cons expr (λ: ["_r"], k ["_r"]) args))%E
   (only parsing, at level 102, f, args, k at level 1) : expr_scope.
 Notation "'letcall:' x := f args 'in' e" :=
   (letcont: "_k" [ x ] := e in call: f args → "_k")%E
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 3375a9cb99da512ad3cc75b5c482c1dadacfc8e0..19c04dd697637ef7dbdec89f960e176d9b8c4d24 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -26,7 +26,7 @@ Section typing.
 
   Lemma type_bool_instr (b : Datatypes.bool) : typed_val #b bool.
   Proof.
-    iIntros (E L tid) "_ _ $ $ _". iApply wp_value.
+    iIntros (E L tid ?) "_ _ $ $ _". iApply wp_value.
     rewrite tctx_interp_singleton tctx_hasty_val' //. by destruct b.
   Qed.
 
@@ -41,7 +41,7 @@ Section typing.
     typed_body E L C T e1 -∗ typed_body E L C T e2 -∗
     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".
+    iIntros (Hp) "He1 He2". iIntros (tid qmax) "#LFT #HE Htl HL HC HT".
     iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "#Hp".
     wp_bind p. iApply (wp_hasty with "Hp").
     iIntros ([[| |[|[]|]]|]) "_ H1"; try done; wp_case.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 146ec89210ea98d8d80e1600a703667fe20a03e0..2df1328be476ad369a69b62210b28b6fe43cbc22 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -14,7 +14,7 @@ Section borrow.
   Lemma tctx_borrow E L p n ty κ :
     tctx_incl E L [p ◁ own_ptr n ty] [p ◁ &uniq{κ}ty; p ◁{κ} own_ptr n ty].
   Proof.
-    iIntros (tid ?)  "#LFT _ $ [H _]".
+    iIntros (tid ??)  "#LFT _ $ [H _]".
     iDestruct "H" as ([[]|]) "[% Hown]"; try done. iDestruct "Hown" as "[Hmt ?]".
     iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
     iModIntro. rewrite /tctx_interp /=. iSplitL "Hbor"; last iSplit; last done.
@@ -25,7 +25,7 @@ Section borrow.
   Lemma tctx_share E L p κ ty :
     lctx_lft_alive E L κ → tctx_incl E L [p ◁ &uniq{κ}ty] [p ◁ &shr{κ}ty].
   Proof.
-    iIntros (Hκ ??) "#LFT #HE HL Huniq".
+    iIntros (Hκ ???) "#LFT #HE HL Huniq".
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; [try done..|].
     rewrite !tctx_interp_singleton /=.
     iDestruct "Huniq" as ([[]|]) "[% Huniq]"; try done.
@@ -86,8 +86,9 @@ Section borrow.
     lctx_lft_alive E L κ →
     ⊢ typed_instruction_ty E L [p ◁ &uniq{κ}(own_ptr n ty)] (!p) (&uniq{κ} ty).
   Proof.
-    iIntros (Hκ tid) "#LFT HE $ HL Hp".
+    iIntros (Hκ tid qmax) "#LFT HE $ HL Hp".
     rewrite tctx_interp_singleton.
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
     wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
     iMod (bor_acc_cons with "LFT Hown Htok") as "[H↦ Hclose']". done.
@@ -97,7 +98,8 @@ Section borrow.
           with "[] [H↦ Hown H†]") as "[Hbor Htok]"; last 1 first.
     - iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
       iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
-      iMod ("Hclose" with "Htok") as "($ & $)".
+      iMod ("Hclose" with "Htok") as "HL".
+      iDestruct ("HLclose" with "HL") as "$".
       by rewrite tctx_interp_singleton tctx_hasty_val' //=.
     - iIntros "!>(?&?&?)!>". iNext. iExists _.
       rewrite -heap_mapsto_vec_singleton. iFrame. by iFrame.
@@ -116,8 +118,9 @@ Section borrow.
     lctx_lft_alive E L κ →
     ⊢ typed_instruction_ty E L [p ◁ &shr{κ}(own_ptr n ty)] (!p) (&shr{κ} ty).
   Proof.
-    iIntros (Hκ tid) "#LFT HE $ HL Hp".
+    iIntros (Hκ tid qmax) "#LFT HE $ HL Hp".
     rewrite tctx_interp_singleton.
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
     iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first solve_ndisj.
     wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
     iDestruct "Hown" as (l') "#[H↦b #Hown]".
@@ -126,7 +129,8 @@ Section borrow.
     - iApply ("Hown" with "[%] Htok2"); first solve_ndisj.
     - iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
       iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
-      iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
+      iMod ("Hclose" with "[Htok1 Htok2]") as "HL"; first by iFrame.
+      iDestruct ("HLclose" with "HL") as "$".
       rewrite tctx_interp_singleton tctx_hasty_val' //. auto.
   Qed.
 
@@ -142,9 +146,10 @@ Section borrow.
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
     ⊢ typed_instruction_ty E L [p ◁ &uniq{κ}(&uniq{κ'}ty)] (!p) (&uniq{κ} ty).
   Proof.
-    iIntros (Hκ Hincl tid) "#LFT #HE $ HL Hp".
+    iIntros (Hκ Hincl tid qmax) "#LFT #HE $ HL Hp".
     rewrite tctx_interp_singleton.
-    iDestruct (Hincl with "HL HE") as "#Hincl".
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
+    iDestruct (Hincl with "HL HE") as "%".
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
     wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
     iMod (bor_exists with "LFT Hown") as (vl) "Hbor". done.
@@ -156,10 +161,11 @@ Section borrow.
     iMod (bor_unnest with "LFT Hbor") as "Hbor"; [done|].
     iApply wp_fupd. wp_read.
     iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]"; first by auto.
-    iMod ("Hclose" with "Htok") as "($ & $)".
+    iMod ("Hclose" with "Htok") as "HL".
+    iDestruct ("HLclose" with "HL") as "$".
     rewrite tctx_interp_singleton tctx_hasty_val' //.
     iApply (bor_shorten with "[] Hbor").
-    iApply (lft_incl_glb with "Hincl"). iApply lft_incl_refl.
+    iApply lft_incl_glb. by iApply lft_incl_syn_sem. iApply lft_incl_refl.
   Qed.
 
   Lemma type_deref_uniq_uniq {E L} κ κ' x p e ty C T T' :
@@ -174,21 +180,25 @@ Section borrow.
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
     ⊢ typed_instruction_ty E L [p ◁ &shr{κ}(&uniq{κ'}ty)] (!p) (&shr{κ}ty).
   Proof.
-    iIntros (Hκ Hincl tid) "#LFT HE $ HL Hp". rewrite tctx_interp_singleton.
-    iDestruct (Hincl with "HL HE") as "#Hincl".
+    iIntros (Hκ Hincl tid qmax) "#LFT HE $ HL Hp". rewrite tctx_interp_singleton.
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
+    iDestruct (Hincl with "HL HE") as "%".
     iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first solve_ndisj.
     wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hshr"; try done.
     iDestruct "Hshr" as (l') "[H↦ Hown]".
     iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
     iAssert (κ ⊑ κ' ⊓ κ)%I as "#Hincl'".
-    { iApply (lft_incl_glb with "Hincl []"). iApply lft_incl_refl. }
+    { iApply lft_incl_glb.
+      + by iApply lft_incl_syn_sem.
+      + by 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 ("Hown" with "[%] Htok2"); first solve_ndisj. }
     iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
     iMod ("Hclose''" with "Htok2") as "Htok2".
     iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
-    iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
+    iMod ("Hclose" with "[Htok1 Htok2]") as "HL"; first by iFrame.
+    iDestruct ("HLclose" with "HL") as "$".
     rewrite tctx_interp_singleton tctx_hasty_val' //.
     by iApply (ty_shr_mono with "Hincl' Hshr").
   Qed.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 74a23f0ff784e31e949857582189bc7ce6e1ffc0..2d7d99ace081b83c2c7215b879016991a5b7b903 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -16,9 +16,11 @@ Section typing.
     tctx_incl E L T (T' (list_to_vec argsv)) →
     ⊢ typed_body E L C T (k args).
   Proof.
-    iIntros (Hargs HC Hincl tid) "#LFT #HE Hna HL HC HT".
+    iIntros (Hargs HC Hincl tid qmax) "#LFT #HE Hna HL HC HT".
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
     iMod (Hincl with "LFT HE HL HT") as "(HL & HT)".
     iSpecialize ("HC" with "[]"); first done.
+    iDestruct ("HLclose" with "HL") as "HL".
     assert (args = of_val <$> argsv) as ->.
     { clear -Hargs. induction Hargs as [|a av ?? [<-%of_to_val| ->] _ ->]=>//=. }
     rewrite -{3}(vec_to_list_to_vec argsv). iApply ("HC" with "Hna HL HT").
@@ -32,7 +34,7 @@ Section typing.
                      (subst_v (kb::argsb) (k:::args) econt)) -∗
     typed_body E L2 C T (letcont: kb argsb := econt in e2).
   Proof.
-    iIntros (Hc1 Hc2) "He2 #Hecont". iIntros (tid) "#LFT #HE Htl HL HC HT".
+    iIntros (Hc1 Hc2) "He2 #Hecont". iIntros (tid qmax) "#LFT #HE Htl HL HC HT".
     rewrite (_ : (rec: kb argsb := econt)%E = of_val (rec: kb argsb := econt)%V); last by unlock.
     wp_let. iApply ("He2" with "LFT HE Htl HL [HC] HT").
     iLöb as "IH". iIntros (x) "H".
@@ -48,7 +50,7 @@ Section typing.
           typed_body E L1 C (T' args) (subst_v (kb :: argsb) (k:::args) econt)) -∗
     typed_body E L2 C T (letcont: kb argsb := econt in e2).
   Proof.
-    iIntros (Hc1 Hc2) "He2 Hecont". iIntros (tid) "#LFT #HE Htl HL HC HT".
+    iIntros (Hc1 Hc2) "He2 Hecont". iIntros (tid qmax) "#LFT #HE Htl HL HC HT".
     rewrite (_ : (rec: kb argsb := econt)%E = of_val (rec: kb argsb := econt)%V); last by unlock.
     wp_let. iApply ("He2" with "LFT HE Htl HL [HC Hecont] HT").
     iIntros (x) "H".
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index f4f3051d8b09c4bd998d1eb2c2827a3da8ef72c9..118434980ae6ff80445a78658c9d73f8f1a92001 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -22,19 +22,19 @@ 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) : iProp Σ :=
+  Definition cctx_elt_interp (tid : thread_id) (qmax: Qp) (x : cctx_elt) : iProp Σ :=
     let '(k ◁cont(L, T)) := x in
-    (∀ args, na_own tid top -∗ llctx_interp L 1 -∗ tctx_interp tid (T args) -∗
+    (∀ args, na_own tid top -∗ llctx_interp qmax L -∗ tctx_interp tid (T args) -∗
          WP k (of_val <$> (args : list _)) {{ _, cont_postcondition }})%I.
-  Definition cctx_interp (tid : thread_id) (C : cctx) : iProp Σ :=
-    (∀ (x : cctx_elt), ⌜x ∈ C⌝ -∗ cctx_elt_interp tid x)%I.
+  Definition cctx_interp (tid : thread_id) (qmax: Qp) (C : cctx) : iProp Σ :=
+    (∀ (x : cctx_elt), ⌜x ∈ C⌝ -∗ cctx_elt_interp tid qmax x)%I.
 
-  Global Instance cctx_interp_permut tid:
-    Proper ((≡ₚ) ==> (⊣⊢)) (cctx_interp tid).
+  Global Instance cctx_interp_permut tid qmax :
+    Proper ((≡ₚ) ==> (⊣⊢)) (cctx_interp tid qmax).
   Proof. solve_proper. Qed.
 
-  Lemma cctx_interp_cons tid x T :
-    cctx_interp tid (x :: T) ≡ (cctx_elt_interp tid x ∧ cctx_interp tid T)%I.
+  Lemma cctx_interp_cons tid qmax x T :
+    cctx_interp tid qmax (x :: T) ≡ (cctx_elt_interp tid qmax x ∧ cctx_interp tid qmax T)%I.
   Proof.
     iSplit.
     - iIntros "H". iSplit; [|iIntros (??)]; iApply "H"; rewrite elem_of_cons; auto.
@@ -43,22 +43,22 @@ Section cont_context.
       + iDestruct "H" as "[_ H]". by iApply "H".
   Qed.
 
-  Lemma cctx_interp_nil tid : cctx_interp tid [] ≡ True%I.
+  Lemma cctx_interp_nil tid qmax : cctx_interp tid qmax [] ≡ True%I.
   Proof. iSplit; first by auto. iIntros "_". iIntros (? Hin). inversion Hin. Qed.
 
-  Lemma cctx_interp_app tid T1 T2 :
-    cctx_interp tid (T1 ++ T2) ≡ (cctx_interp tid T1 ∧ cctx_interp tid T2)%I.
+  Lemma cctx_interp_app tid qmax T1 T2 :
+    cctx_interp tid qmax (T1 ++ T2) ≡ (cctx_interp tid qmax T1 ∧ cctx_interp tid qmax T2)%I.
   Proof.
     induction T1 as [|?? IH]; first by rewrite /= cctx_interp_nil left_id.
     by rewrite /= !cctx_interp_cons IH assoc.
   Qed.
 
-  Lemma cctx_interp_singleton tid x :
-    cctx_interp tid [x] ≡ cctx_elt_interp tid x.
+  Lemma cctx_interp_singleton tid qmax x :
+    cctx_interp tid qmax [x] ≡ cctx_elt_interp tid qmax x.
   Proof. rewrite cctx_interp_cons cctx_interp_nil right_id //. Qed.
 
-  Lemma fupd_cctx_interp tid C :
-    (|={⊤}=> cctx_interp tid C) -∗ cctx_interp tid C.
+  Lemma fupd_cctx_interp tid qmax C :
+    (|={⊤}=> cctx_interp tid qmax C) -∗ cctx_interp tid qmax C.
   Proof.
     rewrite /cctx_interp. iIntros "H". iIntros ([k L n T]) "%".
     iIntros (args) "HL HT". iMod "H".
@@ -66,19 +66,19 @@ Section cont_context.
   Qed.
 
   Definition cctx_incl (E : elctx) (C1 C2 : cctx): Prop :=
-    ∀ tid, lft_ctx -∗ elctx_interp E -∗ cctx_interp tid C1 -∗ cctx_interp tid C2.
+    ∀ tid qmax, lft_ctx -∗ elctx_interp E -∗ cctx_interp tid qmax C1 -∗ cctx_interp tid qmax C2.
 
   Global Instance cctx_incl_preorder E : PreOrder (cctx_incl E).
   Proof.
     split.
-    - iIntros (??) "_ _ $".
-    - iIntros (??? H1 H2 ?) "#LFT #HE HC".
+    - iIntros (???) "_ _ $".
+    - iIntros (??? H1 H2 ??) "#LFT #HE HC".
       iApply (H2 with "LFT HE"). by iApply (H1 with "LFT HE").
   Qed.
 
   Lemma incl_cctx_incl E C1 C2 : C1 ⊆ C2 → cctx_incl E C2 C1.
   Proof.
-    rewrite /cctx_incl /cctx_interp. iIntros (HC1C2 tid) "_ #HE H * %".
+    rewrite /cctx_incl /cctx_interp. iIntros (HC1C2 tid ?) "_ #HE H * %".
     iApply ("H" with "[%]"). by apply HC1C2.
   Qed.
 
@@ -86,10 +86,12 @@ Section cont_context.
     cctx_incl E C1 C2 → (∀ args, tctx_incl E L (T2 args) (T1 args)) →
     cctx_incl E (k ◁cont(L, T1) :: C1) (k ◁cont(L, T2) :: C2).
   Proof.
-    iIntros (HC1C2 HT1T2 ?) "#LFT #HE H". rewrite /cctx_interp.
+    iIntros (HC1C2 HT1T2 ??) "#LFT #HE H". rewrite /cctx_interp.
     iIntros (x) "Hin". iDestruct "Hin" as %[->|Hin]%elem_of_cons.
     - iIntros (args) "Htl HL HT".
+      iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
       iMod (HT1T2 with "LFT HE HL HT") as "(HL & HT)".
+      iDestruct ("HLclose" with "HL") as "HL".
       iApply ("H" $! (_ ◁cont(_, _)) with "[%] Htl HL HT").
       constructor.
     - iApply (HC1C2 with "LFT HE [H] [%]"); last done.
@@ -107,7 +109,7 @@ Section cont_context.
     cctx_incl E C1 (k ◁cont(L, T2) :: C2).
   Proof.
     intros Hin ??. rewrite <-cctx_incl_cons; try done.
-    clear -Hin. iIntros (?) "_ #HE HC".
+    clear -Hin. iIntros (??) "_ #HE HC".
     rewrite cctx_interp_cons. iSplit; last done. clear -Hin.
     iInduction Hin as [] "IH"; rewrite cctx_interp_cons;
       [iDestruct "HC" as "[$ _]" | iApply "IH"; iDestruct "HC" as "[_ $]"].
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
index 372faee59c50774e751dab40420cdd2da0b48f59..36a28ed69cec0809a27be8ed1b182016e49ea515 100644
--- a/theories/typing/examples/nonlexical.v
+++ b/theories/typing/examples/nonlexical.v
@@ -116,7 +116,14 @@ Section non_lexical.
             iIntros (unwrap'). simpl_subst.
           iApply (type_letcall ()); [solve_typing..|]. iIntros (r). simpl_subst.
           iApply type_jump; solve_typing.
-        - iApply type_equivalize_lft.
+        - iApply (type_equivalize_lft _ _ _ _ [_; _; _; _; _; _; _; _]).
+          { iIntros (tid) "#LFT #Hκ1 #Hκ2 ($ & Href & $ & $ & $ & $ & $ & $ & _)".
+            rewrite -tctx_interp_singleton.
+            iApply (type_incl_tctx_incl with "[] Href").
+            iApply own_type_incl; first done.
+            iNext. iApply uniq_type_incl.
+            - iApply "Hκ2".
+            - iApply type_equal_refl. }
           iApply (type_letalloc_n (&uniq{m}V) (own_ptr _ (&uniq{m}V))); [solve_typing..|].
             iIntros (r). simpl_subst.
           iApply type_jump; solve_typing. }
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 58a14e00c32827fbe854262994200ffb67644a89..3efd7862044d39e8d2c981f09251c622ce438b96 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -93,7 +93,7 @@ Section fixpoint.
   Proof.
     unfold eqtype, subtype, type_incl.
     setoid_rewrite <-fixpointK_unfold; [| by apply type_contractive_ne, _..].
-    split; iIntros (qL) "_ !# _"; (iSplit; first done); iSplit; iIntros "!#*$".
+    split; iIntros (qmax qL) "_ !# _"; (iSplit; first done); iSplit; iIntros "!#*$".
   Qed.
 End fixpoint.
 
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 5d9d512b52878d5b640f205cf9f1016cf8407a40..fac54aac4b3fc1fd9446cfd32804359749df1680 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -23,7 +23,7 @@ Section fn.
     {| st_own tid vl := tc_opaque (∃ fb kb xb e H,
          ⌜vl = [@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)  ϝ) [ϝ ⊑ₗ []]
+            □ typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ₗ []]
                          [k◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [(v!!!0%fin:val) ◁ box (fp x).(fp_ty)])]
                          (zip_with (TCtx_hasty ∘ of_val) xl
                                    (box <$> (vec_to_list (fp x).(fp_tys))))
@@ -81,7 +81,8 @@ Section fn.
     (* 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).
+    do 12 f_equiv. f_contractive.
+    do 18 ((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.
@@ -150,7 +151,7 @@ Section typing.
             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".
+    intros Hcons. apply subtype_simple_type=>//= qmax 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) ϝ) ∗
@@ -158,7 +159,7 @@ Section typing.
                  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 (subtype_Forall2_llctx_noend with "HL0") as "#Htys"; first done.
       iDestruct (Hty with "HL0") as "#Hty".
       iClear "∗". iIntros "!# #HEE".
       iSplit; last iSplit.
@@ -167,7 +168,7 @@ Section typing.
       - 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.
+    iExists fb, kb, xb, e, _. iSplit; first done. iSplit; first 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]").
@@ -227,31 +228,31 @@ Section typing.
   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.
+    apply subtype_simple_type=>//= qmax qL.
     iIntros "_ !# _ * Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
-    iExists fb, kb, xb, e, _. iSplit. done. iSplit. done.
+    iExists fb, kb, xb, e, _. iSplit; first done. iSplit; first 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
+  Lemma type_call_iris' E L (κs : list lft) {A} x (ps : list path) qκs qmax 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 ⊤ -∗ llctx_interp L qL -∗
+    lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗ llctx_interp_noend qmax 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 top -∗ llctx_interp L qL -∗ qκs.[lft_intersect_list κs] -∗
+    (∀ ret, na_own tid top -∗ llctx_interp_noend qmax L qL -∗ qκs.[lft_intersect_list κs] -∗
              (box (fp x).(fp_ty)).(ty_own) tid [ret] -∗
              WP k [of_val ret] {{ _, cont_postcondition }}) -∗
     WP (call: p ps → k) {{ _, cont_postcondition }}.
   Proof.
     iIntros (HE [k' <-]) "#LFT #HE Htl HL Hκs Hf Hargs Hk".
     wp_apply (wp_hasty with "Hf"). iIntros (v) "% Hf".
-    iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = (λ: ["_r"], (#☠ ;; #☠) ;; k' ["_r"])%V⌝):::
+    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".
@@ -267,28 +268,37 @@ Section typing.
       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.
+      iMod (lft_create with "LFT") as (ϝ_inner) "[Htk #Hend]"; first done.
+      set (ϝ := ϝ_inner ⊓ lft_intersect_list κs).
       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"); first done. by rewrite Qp_mul_1_r. }
-      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". iModIntro. 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.
+      destruct (Qp_lower_bound qκs 1) as (q0 & q'1 & q'2 & -> & Hsum1).
+      rewrite Hsum1. assert (q0 < 1)%Qp as Hq0.
+      { apply Qp_lt_sum. eauto. }
+      clear Hsum1.
+      iDestruct "Htk" as "[Htk1 Htk2]".
+      iDestruct "Hκs" as "[Hκs1 Hκs2]".
+      iApply ("Hf" $! _ q0 with "LFT [] Htl [Hκs1 Htk1 Htk2] [Hk HL Hκs2]").
+      + iApply "HE'". iFrame "HE".
+        iIntros "{$# Hf Hend HE' LFT HE %}". subst ϝ.
+        iApply big_sepL_forall.
+        iIntros (i [κ1 κ2] [κ [Hpair Helem]]%elem_of_list_lookup_2%elem_of_list_fmap).
+        injection Hpair as -> ->. iPureIntro. simpl.
+        eapply lft_incl_syn_trans; first by apply lft_intersect_incl_syn_r.
+        apply lft_intersect_list_elem_of_incl_syn.
+        done.
+      + iSplitL; last done. iExists ϝ. rewrite left_id. iSplit; first done.
+        rewrite decide_False; last first.
+        { apply Qp_lt_nge. done. }
+        subst ϝ. rewrite -!lft_tok_sep. iFrame. iIntros "[Htk1 _]".
+        rewrite -lft_dead_or. rewrite -bi.or_intro_l. iApply "Hend". iFrame.
+      + iIntros (y) "IN {Hend}". 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 ∪ ↑lft_userN)); first done.
-        iApply (wp_step_fupd with "Hinh"); [set_solver-..|]. 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 /= left_id in EQ. subst κ' ϝ.
+        rewrite decide_False; last first.
+        { apply Qp_lt_nge. done. }
+        rewrite -lft_tok_sep. iDestruct "Htk" as "[_ Hκs1]". wp_rec.
+        iApply ("Hk" with "Htl HL [$Hκs1 $Hκs2]"). 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 !big_sepL_fmap.
         iApply (big_sepL_mono' with "Hvl"); last done. by iIntros (i [v ty']).
@@ -310,7 +320,7 @@ Section typing.
   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.
+    - instantiate (1 := 1%Qp). instantiate (1 := 1%Qp). by rewrite /llctx_interp_noend.
     - iIntros "* Htl _". iApply "Hk". done.
   Qed.
 
@@ -324,7 +334,7 @@ Section typing.
                 T)
                (call: p ps → k).
   Proof.
-    iIntros (Hκs HE tid) "#LFT #HE Htl HL HC (Hf & Hargs & HT)".
+    iIntros (Hκs HE tid qmax) "#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".
@@ -348,8 +358,9 @@ Section typing.
   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; first done. intros args. by inv_vec args.
+    - etrans.
+      + eapply (incl_cctx_incl _ [_]); by intros ? ->%elem_of_list_singleton.
+      + apply cctx_incl_cons; 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.
@@ -376,12 +387,14 @@ Section typing.
         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)).
+      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.
+      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. }
@@ -402,11 +415,11 @@ Section typing.
                      (subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) -∗
     typed_instruction_ty E L T ef (fn fp).
   Proof.
-    iIntros (<- ->) "#Hbody /=". iIntros (tid) "#LFT _ $ $ #HT". iApply wp_value.
+    iIntros (<- ->) "#Hbody /=". iIntros (tid qmax) "#LFT _ $ $ #HT". iApply wp_value.
     rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
     { simpl. rewrite decide_left. done. }
-    iExists fb, _, argsb, e, _. iSplit. done. iSplit. done. iNext.
-    iIntros (x ϝ k args) "!#". iIntros (tid') "_ HE Htl HL HC HT'".
+    iExists fb, _, argsb, e, _. iSplit; first done. iSplit; first done. iNext.
+    iIntros (x ϝ k args) "!#". iIntros (tid' qmax') "_ HE Htl HL HC HT'".
     iApply ("Hbody" with "LFT HE Htl HL HC").
     rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
     by iApply sendc_change_tid.
@@ -417,7 +430,8 @@ Section typing.
     IntoVal ef (funrec: <> argsb := e) →
     n = length argsb →
     □ (∀ x ϝ k (args : vec val (length argsb)),
-        typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ₗ []]
+        typed_body ((fp x).(fp_E) ϝ)
+                   [ϝ ⊑ₗ []]
                    [k ◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [(v!!!0%fin:val) ◁ box (fp x).(fp_ty)])]
                    (zip_with (TCtx_hasty ∘ of_val) args
                              (box <$> vec_to_list (fp x).(fp_tys)) ++ T)
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 56b2cf33146d6b9b0615f3339f586d42c43ee779..c710360d37d9248a0d11644f1705c50c628749b8 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -26,7 +26,7 @@ Section typing.
 
   Lemma type_int_instr (z : Z) : typed_val #z int.
   Proof.
-    iIntros (E L tid) "_ _ $ $ _". iApply wp_value.
+    iIntros (E L tid ?) "_ _ $ $ _". iApply wp_value.
     by rewrite tctx_interp_singleton tctx_hasty_val' //.
   Qed.
 
@@ -39,7 +39,7 @@ Section typing.
   Lemma type_plus_instr E L p1 p2 :
     ⊢ typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 + p2) int.
   Proof.
-    iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
+    iIntros (tid ?) "_ _ $ $ [Hp1 [Hp2 _]]".
     wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
     wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
     wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
@@ -55,7 +55,7 @@ Section typing.
   Lemma type_minus_instr E L p1 p2 :
     ⊢ typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 - p2) int.
   Proof.
-    iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
+    iIntros (tid ?) "_ _ $ $ [Hp1 [Hp2 _]]".
     wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
     wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
     wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
@@ -71,7 +71,7 @@ Section typing.
   Lemma type_le_instr E L p1 p2 :
     ⊢ typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 ≤ p2) bool.
   Proof.
-    iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
+    iIntros (tid ?) "_ _ $ $ [Hp1 [Hp2 _]]".
     wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
     wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
     wp_op; case_bool_decide; by rewrite tctx_interp_singleton tctx_hasty_val' //.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 14744c72e85a1884766261c1abaff29f1ed1efe1..2525bdfc300318fb07ffa9eb407776e19dcacfbf 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -28,7 +28,7 @@ Section lft_contexts.
 
   (* External lifetime contexts. *)
   Definition elctx_elt_interp (x : elctx_elt) : iProp Σ :=
-    (x.1 ⊑ x.2)%I.
+    ⌜(x.1 ⊑ˢʸⁿ x.2)⌝%I.
 
   Definition elctx_interp (E : elctx) : iProp Σ :=
     ([∗ list] x ∈ E, elctx_elt_interp x)%I.
@@ -40,38 +40,80 @@ Section lft_contexts.
   Proof. apply _. Qed.
 
   (* Local lifetime contexts. *)
-  Definition llctx_elt_interp (x : llctx_elt) (q : Qp) : iProp Σ :=
+  (* To support [type_call_iris'], the local lifetime [x.1] may be an
+  intersection of not just the atomic lifetime [κ0] but also of some extra
+  lifetimes [κextra], of which a smaller fraction [qextra] is owned (multiplied
+  by [q] to remain fractional). Since [x.2] is empty, [type_call_iris'] can show
+  that [κ0 ⊓ κextra] is the same after execution the function as it was before,
+  which is sufficient to extract the lifetime tokens for [κextra] again. *)
+  Definition llctx_elt_interp (qmax : Qp) (x : llctx_elt) : iProp Σ :=
     let κ' := lft_intersect_list (x.2) in
-    (∃ κ0, ⌜x.1 = κ' ⊓ κ0⌝ ∗ q.[κ0] ∗ □ (1.[κ0] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†κ0]))%I.
-  Global Instance llctx_elt_interp_fractional x :
-    Fractional (llctx_elt_interp x).
+    (* This is [qeff := min 1 qmax], i.e., we cap qmax at [1] -- but the old
+    std++ we use here does not yet have [min] on [Qp].
+    We do the cap so that we never need to have more than [1] of this token. *)
+    let qeff := (if decide (1 ≤ qmax) then 1 else qmax)%Qp in
+    (∃ κ0, ⌜x.1 = κ' ⊓ κ0⌝ ∗ qeff.[κ0] ∗ (qeff.[κ0] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†κ0]))%I.
+  (* Local lifetime contexts without the "ending a lifetime" viewshifts -- these
+  are fractional. *)
+  Definition llctx_elt_interp_noend (qmax : Qp) (x : llctx_elt) (q : Qp) : iProp Σ :=
+    let κ' := lft_intersect_list (x.2) in
+    let qeff := (if decide (1 ≤ qmax) then 1 else qmax)%Qp in
+    (∃ κ0, ⌜x.1 = κ' ⊓ κ0⌝ ∗ (qeff * q).[κ0])%I.
+  Global Instance llctx_elt_interp_noend_fractional qmax x :
+    Fractional (llctx_elt_interp_noend qmax x).
   Proof.
     destruct x as [κ κs]. iIntros (q q'). iSplit; iIntros "H".
-    - iDestruct "H" as (κ0) "(% & [Hq Hq'] & #?)".
+    - iDestruct "H" as (κ0) "(% & Hq)".
+      rewrite Qp_mul_add_distr_l.
+      iDestruct "Hq" as "[Hq Hq']".
       iSplitL "Hq"; iExists _; by iFrame "∗%".
     - iDestruct "H" as "[Hq Hq']".
-      iDestruct "Hq" as (κ0) "(% & Hq & #?)".
-      iDestruct "Hq'" as (κ0') "(% & Hq' & #?)". simpl in *.
+      iDestruct "Hq" as (κ0) "(% & Hq)".
+      iDestruct "Hq'" as (κ0') "(% & Hq')". simpl in *.
       rewrite (inj ((lft_intersect_list κs) ⊓.) κ0' κ0); last congruence.
-      iExists κ0. by iFrame "∗%".
+      iExists κ0. rewrite Qp_mul_add_distr_l. by iFrame "∗%".
+  Qed.
+
+  Lemma llctx_elt_interp_acc_noend qmax x :
+    llctx_elt_interp qmax x -∗
+    llctx_elt_interp_noend qmax x 1 ∗ (llctx_elt_interp_noend qmax x 1 -∗ llctx_elt_interp qmax x).
+  Proof.
+    destruct x as [κ κs].
+    iIntros "H". iDestruct "H" as (κ0) "(% & Hq & Hend)". iSplitL "Hq".
+    { iExists κ0. rewrite Qp_mul_1_r. by iFrame "∗%". }
+    iIntros "H". iDestruct "H" as (κ0') "(% & Hq')". simpl in *.
+    rewrite (inj ((lft_intersect_list κs) ⊓.) κ0' κ0); last congruence.
+    iExists κ0. rewrite Qp_mul_1_r. by iFrame "∗%".
   Qed.
 
-  Definition llctx_interp (L : llctx) (q : Qp) : iProp Σ :=
-    ([∗ list] x ∈ L, llctx_elt_interp x q)%I.
-  Global Arguments llctx_interp _ _%Qp.
-  Global Instance llctx_interp_fractional L :
-    Fractional (llctx_interp L).
+  Definition llctx_interp (qmax : Qp) (L : llctx) : iProp Σ :=
+    ([∗ list] x ∈ L, llctx_elt_interp qmax x)%I.
+  Definition llctx_interp_noend (qmax : Qp) (L : llctx) (q : Qp) : iProp Σ :=
+    ([∗ list] x ∈ L, llctx_elt_interp_noend qmax x q)%I.
+  Global Instance llctx_interp_fractional qmax L :
+    Fractional (llctx_interp_noend qmax L).
   Proof. intros ??. rewrite -big_sepL_sep. by setoid_rewrite <-fractional. Qed.
-  Global Instance llctx_interp_as_fractional L q :
-    AsFractional (llctx_interp L q) (llctx_interp L) q.
-  Proof. split. done. apply _. Qed.
-  Global Instance llctx_interp_permut :
-    Proper ((≡ₚ) ==> eq ==> (⊣⊢)) llctx_interp.
-  Proof. intros ????? ->. by apply big_opL_permutation. Qed.
-
-  Lemma lctx_equalize_lft qL κ1 κ2 `{!frac_borG Σ} :
-    lft_ctx -∗ llctx_elt_interp (κ1 ⊑ₗ [κ2]%list) qL ={⊤}=∗
-      elctx_elt_interp (κ1 ⊑ₑ κ2) ∗ elctx_elt_interp (κ2 ⊑ₑ κ1).
+  Global Instance llctx_interp_as_fractional qmax L q :
+    AsFractional (llctx_interp_noend qmax L q) (llctx_interp_noend qmax L) q.
+  Proof. split; first done. apply _. Qed.
+  Global Instance llctx_interp_permut qmax :
+    Proper ((≡ₚ) ==> (⊣⊢)) (llctx_interp qmax).
+  Proof. intros ???. by apply big_opL_permutation. Qed.
+
+  Lemma llctx_interp_acc_noend qmax L :
+    llctx_interp qmax L -∗
+    llctx_interp_noend qmax L 1 ∗ (llctx_interp_noend qmax L 1 -∗ llctx_interp qmax L).
+  Proof.
+    rewrite /llctx_interp. setoid_rewrite llctx_elt_interp_acc_noend at 1.
+    rewrite big_sepL_sep. iIntros "[$ Hclose]". iIntros "Hnoend".
+    iCombine "Hclose Hnoend" as "H".
+    rewrite /llctx_interp_noend -big_sepL_sep.
+    setoid_rewrite bi.wand_elim_l. done.
+  Qed.
+
+  Lemma lctx_equalize_lft_sem qmax κ1 κ2 `{!frac_borG Σ} :
+    lft_ctx -∗ llctx_elt_interp qmax (κ1 ⊑ₗ [κ2]%list) ={⊤}=∗
+      κ1 ⊑ κ2 ∗ κ2 ⊑ κ1.
   Proof.
     iIntros "#LFT". iDestruct 1 as (κ) "(% & Hκ & _)"; simplify_eq/=.
     iMod (lft_eternalize with "Hκ") as "#Hincl".
@@ -82,9 +124,9 @@ Section lft_contexts.
       + iApply lft_incl_static.
       + iApply lft_incl_trans; last done. iApply lft_incl_static.
   Qed.
-  Lemma lctx_equalize_lft_static qL κ `{!frac_borG Σ} :
-    lft_ctx -∗ llctx_elt_interp (κ ⊑ₗ []%list) qL ={⊤}=∗
-      elctx_elt_interp (static ⊑ₑ κ).
+  Lemma lctx_equalize_lft_sem_static qmax κ `{!frac_borG Σ} :
+    lft_ctx -∗ llctx_elt_interp qmax (κ ⊑ₗ []%list) ={⊤}=∗
+      static ⊑ κ.
   Proof.
     iIntros "#LFT". iDestruct 1 as (κ') "(% & Hκ & _)"; simplify_eq/=.
     iMod (lft_eternalize with "Hκ") as "#Hincl".
@@ -94,29 +136,41 @@ Section lft_contexts.
       + done.
   Qed.
 
+  (* Lifetime inclusion *)
   Context (E : elctx) (L : llctx).
 
-  (* Lifetime inclusion *)
   Definition lctx_lft_incl κ κ' : Prop :=
-    ∀ qL, llctx_interp L qL -∗ □ (elctx_interp E -∗ κ ⊑ κ').
+    ∀ qmax qL, llctx_interp_noend qmax L qL -∗ □ (elctx_interp E -∗ ⌜κ ⊑ˢʸⁿ κ'⌝)%I.
 
   Definition lctx_lft_eq κ κ' : Prop :=
     lctx_lft_incl κ κ' ∧ lctx_lft_incl κ' κ.
 
-  Lemma lctx_lft_incl_incl κ κ' : lctx_lft_incl κ κ' → lctx_lft_incl κ κ'.
+  Lemma lctx_lft_incl_incl_noend κ κ' : lctx_lft_incl κ κ' → lctx_lft_incl κ κ'.
   Proof. done. Qed.
+  Lemma lctx_lft_incl_incl κ κ' qmax :
+    lctx_lft_incl κ κ' → llctx_interp qmax L -∗ □ (elctx_interp E -∗ ⌜κ ⊑ˢʸⁿ κ'⌝)%I.
+  Proof.
+    iIntros (Hincl) "HL".
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL _]".
+    iApply Hincl. done.
+  Qed.
 
   Lemma lctx_lft_incl_refl κ : lctx_lft_incl κ κ.
-  Proof. iIntros (qL) "_ !# _". iApply lft_incl_refl. Qed.
+  Proof.
+    iIntros (qmax qL) "_ !# _".
+    iPureIntro. apply lft_incl_syn_refl.
+  Qed.
 
   Global Instance lctx_lft_incl_preorder : PreOrder lctx_lft_incl.
   Proof.
     split; first by intros ?; apply lctx_lft_incl_refl.
-    iIntros (??? H1 H2 ?) "HL".
+    iIntros (??? H1 H2 ??) "HL".
     iDestruct (H1 with "HL") as "#H1".
     iDestruct (H2 with "HL") as "#H2".
-    iClear "∗". iIntros "!# #HE". iApply lft_incl_trans.
-    by iApply "H1". by iApply "H2".
+    iClear "∗". iIntros "!# #HE".
+    iDestruct ("H1" with "HE") as "%". iDestruct ("H2" with "HE") as "%".
+    iPureIntro.
+    by eapply lft_incl_syn_trans.
   Qed.
 
   Global Instance lctx_lft_incl_proper :
@@ -132,17 +186,18 @@ Section lft_contexts.
   Qed.
 
   Lemma lctx_lft_incl_static κ : lctx_lft_incl κ static.
-  Proof. iIntros (qL) "_ !# _". iApply lft_incl_static. Qed.
+  Proof. iIntros (qmax qL) "_ !# _". iPureIntro. apply lft_incl_syn_static. Qed.
 
   Lemma lctx_lft_incl_local κ κ' κs :
     κ ⊑ₗ κs ∈ L → κ' ∈ κs → lctx_lft_incl κ κ'.
   Proof.
-    iIntros (? Hκ'κs qL) "H".
+    iIntros (? Hκ'κs qmax qL) "H".
     iDestruct (big_sepL_elem_of with "H") as "H"; first done.
     iDestruct "H" as (κ'') "[EQ _]". iDestruct "EQ" as %EQ.
     simpl in EQ; subst. iIntros "!# #HE".
-    iApply lft_incl_trans; first iApply lft_intersect_incl_l.
-    by iApply lft_intersect_list_elem_of_incl.
+    iPureIntro.
+    eapply lft_incl_syn_trans; first apply lft_intersect_incl_syn_l.
+    by apply lft_intersect_list_elem_of_incl_syn.
   Qed.
 
   Lemma lctx_lft_incl_local' κ κ' κ'' κs :
@@ -151,7 +206,7 @@ Section lft_contexts.
 
   Lemma lctx_lft_incl_external κ κ' : κ ⊑ₑ κ' ∈ E → lctx_lft_incl κ κ'.
   Proof.
-    iIntros (??) "_ !# #HE".
+    iIntros (???) "_ !# #HE".
     rewrite /elctx_interp /elctx_elt_interp big_sepL_elem_of //. done.
   Qed.
 
@@ -161,45 +216,51 @@ Section lft_contexts.
 
   Lemma lctx_lft_incl_intersect κ κ' κ'' :
     lctx_lft_incl κ κ' → lctx_lft_incl κ κ'' →
-    lctx_lft_incl κ (κ' ⊓ κ'').
+    lctx_lft_incl (κ ⊓ κ) (κ' ⊓ κ'').
   Proof.
-    iIntros (Hκ' Hκ'' ?) "HL".
+    iIntros (Hκ' Hκ'' ??) "HL".
     iDestruct (Hκ' with "HL") as "#Hκ'".
     iDestruct (Hκ'' with "HL") as "#Hκ''".
-    iIntros "!# #HE". iApply lft_incl_glb. by iApply "Hκ'". by iApply "Hκ''".
+    iIntros "!# #HE".
+    iDestruct ("Hκ'" with "HE") as "%".
+    iDestruct ("Hκ''" with "HE") as "%".
+    iPureIntro.
+    by apply lft_intersect_mono_syn.
   Qed.
 
   Lemma lctx_lft_incl_intersect_l κ κ' κ'' :
     lctx_lft_incl κ κ' →
     lctx_lft_incl (κ ⊓ κ'') κ'.
   Proof.
-    iIntros (Hκ' ?) "HL".
+    iIntros (Hκ' ??) "HL".
     iDestruct (Hκ' with "HL") as "#Hκ'".
-    iIntros "!# #HE". iApply lft_incl_trans.
-      by iApply lft_intersect_incl_l. by iApply "Hκ'".
+    iIntros "!# #HE". iDestruct ("Hκ'" with "HE") as "%". iPureIntro.
+    eapply lft_incl_syn_trans; last eassumption.
+    by apply lft_intersect_incl_syn_l.
   Qed.
 
   Lemma lctx_lft_incl_intersect_r κ κ' κ'' :
     lctx_lft_incl κ κ' →
     lctx_lft_incl (κ'' ⊓ κ) κ'.
   Proof.
-    iIntros (Hκ' ?) "HL".
+    iIntros (Hκ' ??) "HL".
     iDestruct (Hκ' with "HL") as "#Hκ'".
-    iIntros "!# #HE". iApply lft_incl_trans.
-      by iApply lft_intersect_incl_r. by iApply "Hκ'".
+    iIntros "!# #HE". iDestruct ("Hκ'" with "HE") as "%". iPureIntro.
+    eapply lft_incl_syn_trans; last eassumption.
+    by apply lft_intersect_incl_syn_r.
   Qed.
 
   (* Lifetime aliveness *)
 
   Definition lctx_lft_alive (κ : lft) : Prop :=
-    ∀ F qL, ↑lftN ⊆ F → elctx_interp E -∗ llctx_interp L qL ={F}=∗
-          ∃ q', q'.[κ] ∗ (q'.[κ] ={F}=∗ llctx_interp L qL).
+    ∀ F qmax qL, ↑lftN ⊆ F → elctx_interp E -∗ llctx_interp_noend qmax L qL ={F}=∗
+          ∃ q', q'.[κ] ∗ (q'.[κ] ={F}=∗ llctx_interp_noend qmax L qL).
 
-  Lemma lctx_lft_alive_tok κ F q :
+  Lemma lctx_lft_alive_tok_noend κ F qmax q :
     ↑lftN ⊆ F →
-    lctx_lft_alive κ → elctx_interp E -∗ llctx_interp L q ={F}=∗
-      ∃ q', q'.[κ] ∗ llctx_interp L q' ∗
-                   (q'.[κ] -∗ llctx_interp L q' ={F}=∗ llctx_interp L q).
+    lctx_lft_alive κ → elctx_interp E -∗ llctx_interp_noend qmax L q ={F}=∗
+      ∃ q', q'.[κ] ∗ llctx_interp_noend qmax L q' ∗
+                   (q'.[κ] -∗ llctx_interp_noend qmax L q' ={F}=∗ llctx_interp_noend qmax L q).
   Proof.
     iIntros (? Hal) "#HE [HL1 HL2]".
     iMod (Hal with "HE HL1") as (q') "[Htok Hclose]"; first done.
@@ -209,17 +270,30 @@ Section lft_contexts.
     iApply "Hclose". iFrame.
   Qed.
 
-  Lemma lctx_lft_alive_tok_list κs F q :
+  Lemma lctx_lft_alive_tok κ F qmax :
+    ↑lftN ⊆ F →
+    lctx_lft_alive κ → elctx_interp E -∗ llctx_interp qmax L ={F}=∗
+      ∃ q', q'.[κ] ∗ llctx_interp_noend qmax L q' ∗
+                   (q'.[κ] -∗ llctx_interp_noend qmax L q' ={F}=∗ llctx_interp qmax L).
+  Proof.
+    iIntros (? Hal) "#HE HL".
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
+    iMod (lctx_lft_alive_tok_noend with "HE HL") as (q') "(Hκ & HL & Hclose)"; [done..|].
+    iModIntro. iExists q'. iFrame. iIntros "Hκ HL".
+    iApply "HLclose". iApply ("Hclose" with "Hκ"). done.
+  Qed.
+
+  Lemma lctx_lft_alive_tok_noend_list κs F qmax q :
     ↑lftN ⊆ F → Forall lctx_lft_alive κs →
-      elctx_interp E -∗ llctx_interp L q ={F}=∗
-         ∃ q', q'.[lft_intersect_list κs] ∗ llctx_interp L q' ∗
-                   (q'.[lft_intersect_list κs] -∗ llctx_interp L q' ={F}=∗ llctx_interp L q).
+      elctx_interp E -∗ llctx_interp_noend qmax L q ={F}=∗
+         ∃ q', q'.[lft_intersect_list κs] ∗ llctx_interp_noend qmax L q' ∗
+                   (q'.[lft_intersect_list κs] -∗ llctx_interp_noend qmax L q' ={F}=∗ llctx_interp_noend qmax L q).
   Proof.
     iIntros (? Hκs) "#HE". iInduction κs as [|κ κs] "IH" forall (q Hκs).
     { iIntros "HL !>". iExists _. iFrame "HL". iSplitL; first iApply lft_tok_static.
       iIntros "_ $". done. }
     inversion_clear Hκs.
-    iIntros "HL". iMod (lctx_lft_alive_tok κ with "HE HL") as (q') "(Hκ & HL & Hclose1)"; [solve_typing..|].
+    iIntros "HL". iMod (lctx_lft_alive_tok_noend κ with "HE HL")as (q') "(Hκ & HL & Hclose1)"; [solve_typing..|].
     iMod ("IH" with "[//] HL") as (q'') "(Hκs & HL & Hclose2)".
     destruct (Qp_lower_bound q' q'') as (qq & q0  & q'0 & -> & ->).
     iExists qq. iDestruct "HL" as "[$ HL2]". iDestruct "Hκ" as "[Hκ1 Hκ2]".
@@ -229,46 +303,65 @@ Section lft_contexts.
     iMod ("Hclose1" with "[$Hκ1 $Hκ2] HL") as "HL". done.
   Qed.
 
+  Lemma lctx_lft_alive_tok_list κs F qmax :
+    ↑lftN ⊆ F → Forall lctx_lft_alive κs →
+      elctx_interp E -∗ llctx_interp qmax L ={F}=∗
+         ∃ q', q'.[lft_intersect_list κs] ∗ llctx_interp_noend qmax L q' ∗
+                   (q'.[lft_intersect_list κs] -∗ llctx_interp_noend qmax L q' ={F}=∗ llctx_interp qmax L).
+  Proof.
+    iIntros (? Hal) "#HE HL".
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
+    iMod (lctx_lft_alive_tok_noend_list with "HE HL") as (q') "(Hκ & HL & Hclose)"; [done..|].
+    iModIntro. iExists q'. iFrame. iIntros "Hκ HL".
+    iApply "HLclose". iApply ("Hclose" with "Hκ"). done.
+  Qed.
+
   Lemma lctx_lft_alive_static : lctx_lft_alive static.
   Proof.
-    iIntros (F qL ?) "_ $". iExists 1%Qp. iSplitL. by iApply lft_tok_static. auto.
+    iIntros (F qmax qL ?) "_ $". iExists 1%Qp. iSplitL; last by auto.
+    by iApply lft_tok_static.
   Qed.
 
   Lemma lctx_lft_alive_local κ κs:
     κ ⊑ₗ κs ∈ L → Forall lctx_lft_alive κs → lctx_lft_alive κ.
   Proof.
-    iIntros ([i HL]%elem_of_list_lookup_1 Hκs F qL ?) "#HE HL".
-    iDestruct "HL" as "[HL1 HL2]". rewrite {2}/llctx_interp /llctx_elt_interp.
-    iDestruct (big_sepL_lookup_acc with "HL2") as "[Hκ Hclose]". done.
-    iDestruct "Hκ" as (κ0) "(EQ & Htok & #Hend)". simpl. iDestruct "EQ" as %->.
+    iIntros ([i HL]%elem_of_list_lookup_1 Hκs F qmax qL ?) "#HE HL".
+    iDestruct "HL" as "[HL1 HL2]". rewrite {2}/llctx_interp_noend /llctx_elt_interp.
+    iDestruct (big_sepL_lookup_acc with "HL2") as "[Hκ Hclose]"; first done.
+    iDestruct "Hκ" as (κ0) "(EQ & Htok)". simpl. iDestruct "EQ" as %->.
     iAssert (∃ q', q'.[lft_intersect_list κs] ∗
-      (q'.[lft_intersect_list κs] ={F}=∗ llctx_interp L (qL / 2)))%I
+      (q'.[lft_intersect_list κs] ={F}=∗ llctx_interp_noend qmax L (qL / 2)))%I
       with "[> HE HL1]" as "H".
-    { move:(qL/2)%Qp=>qL'. clear HL. iClear "Hend".
+    { move:(qL/2)%Qp=>qL'. clear HL.
       iInduction Hκs as [|κ κs Hκ ?] "IH" forall (qL').
       - iExists 1%Qp. iFrame. iSplitR; last by auto. iApply lft_tok_static.
       - iDestruct "HL1" as "[HL1 HL2]".
-        iMod (Hκ with "HE HL1") as (q') "[Htok' Hclose]". done.
+        iMod (Hκ with "HE HL1") as (q') "[Htok' Hclose]"; first done.
         iMod ("IH" with "HL2") as (q'') "[Htok'' Hclose']".
         destruct (Qp_lower_bound q' q'') as (q0 & q'2 & q''2 & -> & ->).
         iExists q0. rewrite -lft_tok_sep. iDestruct "Htok'" as "[$ Hr']".
         iDestruct "Htok''" as "[$ Hr'']". iIntros "!>[Hκ Hfold]".
         iMod ("Hclose" with "[$Hκ $Hr']") as "$". iApply "Hclose'". iFrame. }
     iDestruct "H" as (q') "[Htok' Hclose']". rewrite -{5}(Qp_div_2 qL).
-    destruct (Qp_lower_bound q' (qL/2)) as (q0 & q'2 & q''2 & -> & ->).
-    iExists q0. rewrite -(lft_tok_sep q0). iDestruct "Htok" as "[$ Htok]".
+    set (qeff := (if decide (1 ≤ qmax) then 1 else qmax)%Qp).
+    destruct (Qp_lower_bound q' (qeff * (qL/2))) as (q0 & q'2 & q''2 & -> & Hmax).
+    iExists q0. rewrite -(lft_tok_sep q0). rewrite Hmax.
+    iDestruct "Htok" as "[$ Htok]".
     iDestruct "Htok'" as "[$ Htok']". iIntros "!>[Hfold Hκ0]".
     iMod ("Hclose'" with "[$Hfold $Htok']") as "$".
-    rewrite /llctx_interp /llctx_elt_interp. iApply "Hclose". iExists κ0. iFrame. auto.
+    rewrite /llctx_interp /llctx_elt_interp. iApply "Hclose".
+    iExists κ0. rewrite Hmax. iFrame. auto.
   Qed.
 
   Lemma lctx_lft_alive_incl κ κ':
     lctx_lft_alive κ → lctx_lft_incl κ κ' → lctx_lft_alive κ'.
   Proof.
-    iIntros (Hal Hinc F qL ?) "#HE HL".
-    iAssert (κ ⊑ κ')%I with "[#]" as "#Hincl". iApply (Hinc with "HL HE").
-    iMod (Hal with "HE HL") as (q') "[Htok Hclose]". done.
-    iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose']". done.
+    iIntros (Hal Hinc F qmax qL ?) "#HE HL".
+    iAssert (κ ⊑ κ')%I with "[#]" as "#Hincl".
+    { rewrite Hinc. iDestruct ("HL" with "HE") as "%".
+      by iApply lft_incl_syn_sem. }
+    iMod (Hal with "HE HL") as (q') "[Htok Hclose]"; first done.
+    iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose']"; first done.
     iExists q''. iIntros "{$Htok}!>Htok". iApply ("Hclose" with "[> -]").
     by iApply "Hclose'".
   Qed.
@@ -282,15 +375,15 @@ Section lft_contexts.
   (* External lifetime context satisfiability *)
 
   Definition elctx_sat E' : Prop :=
-    ∀ qL, llctx_interp L qL -∗ □ (elctx_interp E -∗ elctx_interp E').
+    ∀ qmax qL, llctx_interp_noend qmax L qL -∗ □ (elctx_interp E -∗ elctx_interp E').
 
   Lemma elctx_sat_nil : elctx_sat [].
-  Proof. iIntros (?) "_ !# _". by rewrite /elctx_interp /=. Qed.
+  Proof. iIntros (??) "_ !# _". by rewrite /elctx_interp /=. Qed.
 
   Lemma elctx_sat_lft_incl E' κ κ' :
     lctx_lft_incl κ κ' → elctx_sat E' → elctx_sat ((κ ⊑ₑ κ') :: E').
   Proof.
-    iIntros (Hκκ' HE' qL) "HL".
+    iIntros (Hκκ' HE' qmax qL) "HL".
     iDestruct (Hκκ' with "HL") as "#Hincl".
     iDestruct (HE' with "HL") as "#HE'".
     iClear "∗". iIntros "!# #HE". iSplit.
@@ -301,7 +394,7 @@ Section lft_contexts.
   Lemma elctx_sat_app E1 E2 :
     elctx_sat E1 → elctx_sat E2 → elctx_sat (E1 ++ E2).
   Proof.
-    iIntros (HE1 HE2 ?) "HL".
+    iIntros (HE1 HE2 ??) "HL".
     iDestruct (HE1 with "HL") as "#HE1".
     iDestruct (HE2 with "HL") as "#HE2".
     iClear "∗". iIntros "!# #HE".
@@ -310,19 +403,21 @@ Section lft_contexts.
   Qed.
 
   Lemma elctx_sat_refl : elctx_sat E.
-  Proof. iIntros (?) "_ !# ?". done. Qed.
+  Proof. iIntros (??) "_ !# ?". done. Qed.
 End lft_contexts.
 
-Arguments lctx_lft_incl {_ _ _} _ _ _ _.
-Arguments lctx_lft_eq {_ _ _} _ _ _ _.
+Arguments lctx_lft_incl {_ _} _ _ _ _.
+Arguments lctx_lft_eq {_ _} _ _ _ _.
 Arguments lctx_lft_alive {_ _ _} _ _ _.
-Arguments elctx_sat {_ _ _} _ _ _.
+Arguments elctx_sat {_ _} _ _ _.
 Arguments lctx_lft_incl_incl {_ _ _ _ _} _ _.
+Arguments lctx_lft_incl_incl_noend {_ _ _ _} _ _.
 Arguments lctx_lft_alive_tok {_ _ _ _ _} _ _ _.
+Arguments lctx_lft_alive_tok_noend {_ _ _ _ _} _ _ _.
 
 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.
+Proof. iIntros (HE' ??) "_ !# H". by iApply big_sepL_submseteq. Qed.
 
 Hint Resolve
      lctx_lft_incl_refl lctx_lft_incl_static lctx_lft_incl_local'
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index cb9d8f8efec9d118b4e6063b43035073ccf6c593..88ad58aaa16e503c3defea1627ec8f4dcd4229af 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -194,7 +194,7 @@ Section arc.
   Global Instance arc_mono E L :
     Proper (subtype E L ==> subtype E L) arc.
   Proof.
-    iIntros (ty1 ty2 Hsub ?) "HL". iDestruct (Hsub with "HL") as "#Hsub".
+    iIntros (ty1 ty2 Hsub ??) "HL". iDestruct (Hsub with "HL") as "#Hsub".
     iIntros "!# #HE". iApply arc_subtype. by iApply "Hsub".
   Qed.
   Global Instance arc_proper E L :
@@ -303,7 +303,7 @@ Section arc.
   Global Instance weak_mono E L :
     Proper (subtype E L ==> subtype E L) weak.
   Proof.
-    iIntros (ty1 ty2 Hsub ?) "HL". iDestruct (Hsub with "HL") as "#Hsub".
+    iIntros (ty1 ty2 Hsub ??) "HL". iDestruct (Hsub with "HL") as "#Hsub".
     iIntros "!# #HE". iApply weak_subtype. by iApply "Hsub".
   Qed.
   Global Instance weak_proper E L :
@@ -344,7 +344,7 @@ Section arc.
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_new (2 + ty.(ty_size))); [solve_typing..|]; iIntros (rcbox); simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (rc); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hrc [Hrcbox [Hx _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrc [Hrcbox [Hx _]]]".
     rewrite !tctx_hasty_val.
     iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
     iDestruct (ownptr_uninit_own with "Hrcbox")
@@ -386,7 +386,7 @@ Section arc.
       iIntros (_ ϝ ret arg). inv_vec arg. simpl_subst.
     iApply (type_new (2 + ty.(ty_size))); [solve_typing..|]; iIntros (rcbox); simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (rc); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hrc [Hrcbox _]]". rewrite !tctx_hasty_val.
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrc [Hrcbox _]]". rewrite !tctx_hasty_val.
     iDestruct (ownptr_uninit_own with "Hrcbox")
       as (lrcbox vlrcbox) "(% & Hrcbox↦ & Hrcbox†)". subst rcbox. inv_vec vlrcbox=>??? /=.
     iDestruct (heap_mapsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
@@ -427,7 +427,7 @@ Section arc.
       iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (x); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [#Hrc' [Hx _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrcx [#Hrc' [Hx _]]]".
     rewrite !tctx_hasty_val [[rcx]]lock.
     iDestruct (ownptr_uninit_own with "Hx") as (lrc2 vlrc2) "(% & Hx & Hx†)".
     subst x. inv_vec vlrc2=>?. rewrite heap_mapsto_vec_singleton.
@@ -471,7 +471,7 @@ Section arc.
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     (* All right, we are done preparing our context. Let's get going. *)
@@ -514,7 +514,7 @@ Section arc.
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     (* All right, we are done preparing our context. Let's get going. *)
@@ -559,7 +559,7 @@ Section arc.
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     (* All right, we are done preparing our context. Let's get going. *)
@@ -603,7 +603,7 @@ Section arc.
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     (* All right, we are done preparing our context. Let's get going. *)
@@ -647,7 +647,7 @@ Section arc.
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     (* All right, we are done preparing our context. Let's get going. *)
@@ -694,7 +694,7 @@ Section arc.
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     (* All right, we are done preparing our context. Let's get going. *)
@@ -753,7 +753,7 @@ Section arc.
     iApply (type_new (option ty).(ty_size)); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iApply (type_sum_unit (option ty)); [solve_typing..|].
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hr [Hrcx [Hrc' _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hr [Hrcx [Hrc' _]]]".
     rewrite !tctx_hasty_val. destruct rc' as [[|rc'|]|]=>//=.
     iAssert (shared_arc_own rc' ty tid)%I with "[>Hrc']" as "Hrc'".
     { iDestruct "Hrc'" as "[?|$]"; last done. iApply arc_own_share; solve_ndisj. }
@@ -815,7 +815,7 @@ Section arc.
     iIntros (_ ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
     iApply (type_new 0); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock. destruct rc' as [[|rc'|]|]=>//=.
     iDestruct "Hrc'" as (γ ν) "[#Hpersist Htok]". wp_bind (drop_weak _).
     iApply (drop_weak_spec with "[] [Htok]"); [by iDestruct "Hpersist" as "[$?]"|by auto|].
@@ -859,7 +859,7 @@ Section arc.
     iApply (type_new (Σ[ ty; arc ty ]).(ty_size));
       [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock. destruct rc' as [[|rc'|]|]=>//=.
     iAssert (shared_arc_own rc' ty tid)%I with "[>Hrc']" as "Hrc'".
     { iDestruct "Hrc'" as "[?|$]"; last done. iApply arc_own_share; solve_ndisj. }
@@ -932,7 +932,7 @@ Section arc.
     iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
     iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock. destruct rc' as [[|rc'|]|]=>//=.
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & HL & Hclose1)";
       [solve_typing..|].
@@ -1020,7 +1020,7 @@ Section arc.
     iIntros "/= !#". iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock. destruct rc' as [[|rc'|]|]=>//=.
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)";
       [solve_typing..|].
@@ -1080,7 +1080,7 @@ Section arc.
       rewrite heap_mapsto_vec_singleton. wp_write. wp_let.
       wp_bind (of_val clone).
       iApply (wp_wand with "[Hna]").
-      { iApply (Hclone _ [] with "LFT HE Hna"); rewrite /llctx_interp /tctx_interp //. }
+      { iApply (Hclone _ [] $! _ 1%Qp with "LFT HE Hna"); rewrite /llctx_interp /tctx_interp //. }
       clear Hclone clone. iIntros (clone) "(Hna & _ & [Hclone _])". rewrite tctx_hasty_val.
       iDestruct "Hs" as "[Hs|Hν']"; last by iDestruct (lft_tok_dead with "Hν Hν'") as "[]".
       iDestruct (lft_intersect_acc with "Hα2 Hν") as (q'') "[Hαν Hclose3]".
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index d023ae35ac61efd0cffdf6d0a49202bf278b2d4e..ae86479bff86846a560cd4278f40e03cd13b5fd8 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -34,7 +34,7 @@ Section cell.
 
   Global Instance cell_mono E L : Proper (eqtype E L ==> subtype E L) cell.
   Proof.
-    move=>?? /eqtype_unfold EQ. iIntros (?) "HL".
+    move=>?? /eqtype_unfold EQ. iIntros (??) "HL".
     iDestruct (EQ with "HL") as "#EQ". iIntros "!# #HE".
     iDestruct ("EQ" with "HE") as "(% & #Hown & #Hshr)".
     iSplit; [done|iSplit; iIntros "!# * H"].
@@ -91,7 +91,7 @@ Section typing.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_jump; [solve_typing..|].
-    iIntros (??) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
+    iIntros (???) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
   Qed.
 
   (* The other direction: getting ownership out of a cell. *)
@@ -103,7 +103,7 @@ Section typing.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_jump; [solve_typing..|].
-    iIntros (??) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
+    iIntros (???) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
   Qed.
 
   Definition cell_get_mut : val :=
@@ -115,7 +115,7 @@ Section typing.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_jump; [solve_typing..|].
-    iIntros (??) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
+    iIntros (???) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
   Qed.
 
   Definition cell_from_mut : val :=
@@ -127,7 +127,7 @@ Section typing.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_jump; [solve_typing..|].
-    iIntros (??) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
+    iIntros (???) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
   Qed.
 
   Definition cell_into_box : val :=
@@ -139,7 +139,7 @@ Section typing.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_jump; [solve_typing..|].
-    iIntros (??) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
+    iIntros (???) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
   Qed.
 
   Definition cell_from_box : val :=
@@ -151,7 +151,7 @@ Section typing.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_jump; [solve_typing..|].
-    iIntros (??) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
+    iIntros (???) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
   Qed.
 
   (** Reading from a cell *)
@@ -192,7 +192,7 @@ Section typing.
     iIntros (c'); simpl_subst.
     iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
     (* Drop to Iris level. *)
-    iIntros (tid) "#LFT #HE Htl HL HC".
+    iIntros (tid qmax) "#LFT #HE Htl HL HC".
     rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iIntros "(Hr & Hc & #Hc' & Hx)".
     destruct c' as [[|c'|]|]; try done. destruct x as [[|x|]|]; try done.
@@ -241,7 +241,7 @@ Section typing.
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk HT".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk HT".
     rewrite tctx_interp_singleton tctx_hasty_val.
     iApply (type_type _ _ _ [ x ◁ box (&uniq{α}(cell ty)) ]
             with "[] LFT HE Hna HL Hk [HT]"); last first.
diff --git a/theories/typing/examples/diverging_static.v b/theories/typing/lib/diverging_static.v
similarity index 57%
rename from theories/typing/examples/diverging_static.v
rename to theories/typing/lib/diverging_static.v
index fd1ec12b113b9a73cc0f0fda6b822b8de592658d..93bebbe25d0a1d0fcf10310228887099a464d14f 100644
--- a/theories/typing/examples/diverging_static.v
+++ b/theories/typing/lib/diverging_static.v
@@ -27,19 +27,37 @@ Section diverging_static.
     intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x f. simpl_subst.
     iApply type_let; [apply Hf|solve_typing|]. iIntros (call); simpl_subst.
-    iApply (type_cont [_] [] (λ r, [(r!!!0%fin:val) ◁ box (unit)])).
-    { iIntros (k). simpl_subst.
-      iApply type_equivalize_lft_static.
-      iApply (type_call [ϝ] ()); solve_typing. }
-    iIntros "!# *". inv_vec args=>r. simpl_subst.
-    iApply (type_cont [] [] (λ r, [])).
-    { iIntros (kloop). simpl_subst. iApply type_jump; solve_typing. }
-    iIntros "!# *". inv_vec args. simpl_subst.
-    iApply type_jump; solve_typing.
+    (* Drop to Iris *)
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk (Hcall & Hx & Hf & _)".
+    (* We need a ϝ token to show that we can call F despite it being non-'static. *)
+    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (qϝ) "(Hϝ & HL & _)";
+      [solve_typing..|].
+    iMod (lctx_lft_alive_tok_noend α with "HE HL") as (q) "(Hα & _ & _)";
+      [solve_typing..|].
+    iMod (lft_eternalize with "Hα") as "#Hα".
+    iAssert (type_incl (box (&shr{α} T)) (box (&shr{static} T))) as "#[_ [Hincl _]]".
+    { iApply box_type_incl. iNext. iApply shr_type_incl; first done.
+      iApply type_incl_refl. }
+    wp_let. rewrite tctx_hasty_val.
+    iApply (type_call_iris _ [ϝ] () [_; _] with "LFT HE Hna [Hϝ] Hcall [Hx Hf]").
+    - solve_typing.
+    - by rewrite /= (right_id static).
+    - simpl. iFrame. iSplit; last done. rewrite !tctx_hasty_val.
+      iApply "Hincl". done.
+    - iClear "Hα Hincl". iIntros (r) "Htl Hϝ1 Hret". wp_rec.
+      (* Go back to the type system. *)
+      iApply (type_type _ [] _ [] with "[] LFT HE Htl [] Hk [-]"); last first.
+      { rewrite /tctx_interp /=. done. }
+      { rewrite /llctx_interp /=. done. }
+      iApply (type_cont [] [] (λ _, [])).
+      + iIntros (?). simpl_subst. iApply type_jump; solve_typing.
+      + iIntros "!#" (? args). inv_vec args. simpl_subst. iApply type_jump; solve_typing.
   Qed.
 
-  (** Variant of the above where the lifetime is in an arbitrary invariant
-      position.  This is incompatible with branding!
+
+  (** With the right typing rule, we can prove a variant of the above where the
+      lifetime is in an arbitrary invariant position, without even leaving the
+      type system.  This is incompatible with branding!
 
       Our [TyWf] is not working well for type constructors (we have no way of
       representing the fact that well-formedness is somewhat "uniform"), so we
@@ -49,8 +67,13 @@ Section diverging_static.
       list would require some induction-based reasoning principles that we do
       not have, but showing that it works for one lifetime is enough to
       demonstrate the principle). *)
-  Lemma diverging_static_loop_type' (T : lft → type) F κuser Euser call_once
+  Lemma diverging_static_loop_type_bad (T : lft → type) F κuser Euser call_once
         `{!TyWf F} :
+    (* The "bad" type_equivalize_lft_static rule *)
+    (∀ E L C T κ e,
+      (⊢ typed_body ((static ⊑ₑ κ) :: E) L C T e) →
+      ⊢ typed_body E ((κ ⊑ₗ []) :: L) C T e) →
+    (* Typing of this function *)
     let _ : (∀ κ, TyWf (T κ)) := λ κ, {| ty_lfts := [κ; κuser]; ty_wf_E := Euser |} in
     (∀ κ1 κ2, (T κ1).(ty_size) = (T κ2).(ty_size)) →
     (∀ E L κ1 κ2, lctx_lft_eq E L κ1 κ2 → subtype E L (T κ1) (T κ2)) →
@@ -58,12 +81,13 @@ Section diverging_static.
     typed_val (diverging_static_loop call_once)
               (fn(∀ α, ∅; T α, F) → ∅).
   Proof.
-    intros HWf HTsz HTsub Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    intros type_equivalize_lft_static_bad HWf HTsz HTsub Hf E L.
+    iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x f. simpl_subst.
     iApply type_let; [apply Hf|solve_typing|]. iIntros (call); simpl_subst.
     iApply (type_cont [_] [] (λ r, [(r!!!0%fin:val) ◁ box (unit)])).
     { iIntros (k). simpl_subst.
-      iApply type_equivalize_lft_static.
+      iApply type_equivalize_lft_static_bad.
       iApply (type_call [ϝ] ()); solve_typing. }
     iIntros "!# *". inv_vec args=>r. simpl_subst.
     iApply (type_cont [] [] (λ r, [])).
@@ -71,5 +95,4 @@ Section diverging_static.
     iIntros "!# *". inv_vec args. simpl_subst.
     iApply type_jump; solve_typing.
   Qed.
-
 End diverging_static.
diff --git a/theories/typing/lib/fake_shared.v b/theories/typing/lib/fake_shared.v
index 384b44cf7e33b0d37a6b5a85eb4f0effa9c02981..9d6b7152b590e2cc57116d299c4209a37126773a 100644
--- a/theories/typing/lib/fake_shared.v
+++ b/theories/typing/lib/fake_shared.v
@@ -14,9 +14,9 @@ Section fake_shared.
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk HT".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk HT".
     rewrite tctx_interp_singleton tctx_hasty_val.
-    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "%"; [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.
@@ -25,7 +25,8 @@ Section fake_shared.
       { iApply frac_bor_iff; last done. iIntros "!>!# *".
         rewrite heap_mapsto_vec_singleton. iSplit; auto. }
       iDestruct "H" as "#H". iIntros "!# * % $". iApply step_fupd_intro. set_solver.
-      simpl. by iApply ty_shr_mono. }
+      simpl. iApply ty_shr_mono; last done.
+      by iApply lft_incl_syn_sem. }
     do 2 wp_seq.
     iApply (type_type [] _ _ [ x ◁ box (&shr{α}(box ty)) ]
             with "[] LFT [] Hna HL Hk [HT]"); last first.
@@ -43,9 +44,9 @@ Section fake_shared.
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk HT".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk HT".
     rewrite tctx_interp_singleton tctx_hasty_val.
-    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "%"; [solve_typing..|].
     (* FIXME: WTF, using &uniq{β} here does not work. *)
     iAssert (▷ ty_own (own_ptr 1 (&shr{α} (uniq_bor β ty))) tid [x])%I with "[HT]" as "HT".
     { destruct x as [[|l|]|]=>//=. iDestruct "HT" as "[H $]".
@@ -55,7 +56,9 @@ Section fake_shared.
       { iApply frac_bor_iff; last done. iIntros "!>!# *".
         rewrite heap_mapsto_vec_singleton. iSplit; auto. }
       iDestruct "H" as "#H". iIntros "!# * % $". iApply step_fupd_intro. set_solver.
-      simpl. iApply ty_shr_mono; last done. iApply lft_intersect_incl_l. }
+      simpl. iApply ty_shr_mono; last done.
+      by iApply lft_intersect_incl_l.
+    }
     do 2 wp_seq.
     iApply (type_type [] _ _ [ x ◁ box (&shr{α}(&uniq{β} ty)) ]
             with "[] LFT [] Hna HL Hk [HT]"); last first.
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index c92f87bd17368db5ee5a3de11a3a9e4cf3124af8..d73ae6d55568cf28c4d678ab1243508d1e385f8f 100644
--- a/theories/typing/lib/join.v
+++ b/theories/typing/lib/join.v
@@ -43,7 +43,7 @@ Section join.
     iApply type_let; [apply HfA|solve_typing|]. iIntros (fA); simpl_subst.
     iApply type_let; [apply HfB|solve_typing|]. iIntros (fB); simpl_subst.
     (* Drop to Iris. *)
-    iIntros (tid) "#LFT #HE Hna HL Hk (HfB & HfA & HenvA & HenvB & _)".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk (HfB & HfA & HenvA & HenvB & _)".
     iMod (lctx_lft_alive_tok ϝ with "HE HL") as (qϝ1) "(Hϝ1 & HL & Hclose1)";
       [solve_typing..|].
     (* FIXME: using wp_apply here breaks calling solve_to_val. *)
@@ -60,7 +60,7 @@ Section join.
         wp_rec. iApply (finish_spec with "[$Hfin Hret Hϝ1]"); last auto.
         rewrite right_id. iFrame. by iApply @send_change_tid. }
     iNext. iIntros (c) "Hjoin". wp_let. wp_let.
-    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (qϝ2) "(Hϝ2 & HL & Hclose2)";
+    iMod (lctx_lft_alive_tok_noend ϝ with "HE HL") as (qϝ2) "(Hϝ2 & HL & Hclose2)";
       [solve_typing..|].
     rewrite !tctx_hasty_val.
     iApply (type_call_iris _ [ϝ] () [_] with "LFT HE Hna [Hϝ2] HfB [HenvB]").
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index cf3f8f6b244eff1b05c283120a911a136caeb05f..70b5b362560d79159928db8b7905f8d125fb8eb2 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -89,7 +89,7 @@ Section mutex.
 
   Global Instance mutex_mono E L : Proper (eqtype E L ==> subtype E L) mutex.
   Proof.
-    move=>ty1 ty2 /eqtype_unfold EQ. iIntros (?) "HL".
+    move=>ty1 ty2 /eqtype_unfold EQ. iIntros (??) "HL".
     iDestruct (EQ with "HL") as "#EQ". iIntros "!# #HE". clear EQ.
     iDestruct ("EQ" with "HE") as "(% & #Howni & _) {EQ}".
     iSplit; last iSplit.
@@ -146,7 +146,7 @@ Section code.
     (* FIXME: The following should work.  We could then go into Iris later.
     iApply (type_memcpy ty); [solve_typing..|]. *)
     (* Switch to Iris. *)
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hm [Hx _]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hm [Hx _]]".
     rewrite !tctx_hasty_val /=.
     iDestruct (ownptr_uninit_own with "Hm") as (lm vlm) "(% & Hm & Hm†)".
     subst m. inv_vec vlm=>m vlm. simpl. iDestruct (heap_mapsto_vec_cons with "Hm") as "[Hm0 Hm]".
@@ -181,7 +181,7 @@ Section code.
       iIntros (_ ϝ ret arg). inv_vec arg=>m. simpl_subst.
     iApply (type_new ty.(ty_size)); [solve_typing..|]; iIntros (x); simpl_subst.
     (* Switch to Iris. *)
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hm _]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hx [Hm _]]".
     rewrite !tctx_hasty_val /=.
     iDestruct (ownptr_uninit_own with "Hx") as (lx vlx) "(% & Hx & Hx†)".
     subst x. simpl.
@@ -220,7 +220,7 @@ Section code.
       iIntros (α ϝ ret arg); inv_vec arg=>m; simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (m'); simpl_subst.
     (* Go to Iris *)
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hm [Hm' _]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hm [Hm' _]]".
     rewrite !tctx_hasty_val [[m]]lock.
     destruct m' as [[|lm'|]|]; try done. simpl.
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose1)";
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 0bb64a0016762cb271a7cde3fa0d1fe66073cec3..d57fac593c7f1a36a3ab87c16359b1e46d57a9a5 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -87,15 +87,16 @@ Section mguard.
   Global Instance mutexguard_mono E L :
     Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) mutexguard.
   Proof.
-    intros α1 α2 Hα ty1 ty2 Hty. generalize Hty. rewrite eqtype_unfold. iIntros (Hty' q) "HL".
+    intros α1 α2 Hα ty1 ty2 Hty. generalize Hty. rewrite eqtype_unfold.
+    iIntros (Hty' qmax qL) "HL".
     iDestruct (Hty' with "HL") as "#Hty". clear Hty'. iDestruct (Hα with "HL") as "#Hα".
-    iIntros "!# #HE". iDestruct ("Hα" with "HE") as "{Hα} Hα".
+    iIntros "!# #HE". iDestruct ("Hα" with "HE") as %Hα12.
     iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs) {HE Hty}". iSplit; [done|iSplit; iModIntro].
     - iIntros (tid [|[[]|][]]) "H"; try done. simpl.
       iDestruct "H" as (β) "(#H⊑ & #Hinv & Hown)".
       iExists β. iFrame. iSplit; last iSplit.
-      + by iApply lft_incl_trans.
-      + iApply (at_bor_shorten with "Hα").
+      + iApply lft_incl_trans; first by iApply lft_incl_syn_sem. done.
+      + iApply at_bor_shorten; first by iApply lft_incl_syn_sem.
         iApply (at_bor_iff with "[] Hinv"). iNext.
         iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
         iApply heap_mapsto_pred_iff_proper.
@@ -106,11 +107,13 @@ Section mguard.
     - iIntros (κ tid l) "H". iDestruct "H" as (l') "H". iExists l'.
       iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
       iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
-      { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
+      { iApply lft_intersect_mono; first by iApply lft_incl_syn_sem. iApply lft_incl_refl. }
       iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
       iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
-      iApply ty_shr_mono; try done. iApply lft_intersect_mono. done. iApply lft_incl_refl.
-      by iApply "Hs".
+      iApply ty_shr_mono; try done.
+      + iApply lft_intersect_mono; first by iApply lft_incl_syn_sem.
+        iApply lft_incl_refl.
+      + by iApply "Hs".
   Qed.
 
   Global Instance mutexguard_proper E L :
@@ -172,7 +175,7 @@ Section code.
     iApply type_deref; [solve_typing..|]; iIntros (m); simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (g); simpl_subst.
     (* Switch to Iris. *)
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hg [Hx [Hm _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hg [Hx [Hm _]]]".
     rewrite !tctx_hasty_val [[x]]lock /=.
     destruct m as [[|lm|]|]; try done. iDestruct "Hm" as (κ') "[#Hακ' #Hshr]".
     iDestruct (ownptr_uninit_own with "Hg") as (lg vlg) "(% & Hg & Hg†)".
@@ -208,7 +211,7 @@ Section code.
       iIntros ([α β] ϝ ret arg). inv_vec arg=>g. simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (g'); simpl_subst.
     (* Switch to Iris. *)
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hg [Hg' _]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hg [Hg' _]]".
     rewrite !tctx_hasty_val [[g]]lock /=.
     destruct g' as [[|lg|]|]; try done. simpl.
     iMod (bor_exists with "LFT Hg'") as (vl) "Hbor"; first done.
@@ -225,7 +228,7 @@ Section code.
     iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hclose2]"; first done.
     wp_bind (!_)%E. iMod (bor_unnest with "LFT Hlm") as "Hlm"; first done.
     wp_read. wp_let. iMod "Hlm".
-    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    iDestruct (lctx_lft_incl_incl_noend α β with "HL HE") as "%"; [solve_typing..|].
     iMod ("Hclose2" with "H↦") as "[_ Hα]".
     iMod ("Hclose1" with "Hα HL") as "HL".
     (* Switch back to typing mode. *)
@@ -234,7 +237,7 @@ Section code.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       unlock. iFrame. iApply bor_shorten; last done.
       iApply lft_incl_glb; last by iApply lft_incl_refl.
-      iApply lft_incl_trans; done. }
+      iApply lft_incl_trans; last done. by iApply lft_incl_syn_sem. }
     iApply type_letalloc_1; [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -250,14 +253,14 @@ Section code.
       iIntros ([α β] ϝ ret arg). inv_vec arg=>g. simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (g'); simpl_subst.
     (* Switch to Iris. *)
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hg [Hg' _]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hg [Hg' _]]".
     rewrite !tctx_hasty_val [[g]]lock /=.
     destruct g' as [[|lg|]|]; try done. simpl.
     iDestruct "Hg'" as (lm) "[Hlg Hshr]".
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose1)";
       [solve_typing..|].
     iMod (frac_bor_acc with "LFT Hlg Hα1") as (qlx') "[H↦ Hclose2]"; first done.
-    iMod (lctx_lft_alive_tok β with "HE HL") as (qβ) "(Hβ & HL & Hclose3)";
+    iMod (lctx_lft_alive_tok_noend β with "HE HL") as (qβ) "(Hβ & HL & Hclose3)";
       [solve_typing..|].
     iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hclose4]".
     wp_bind (!_)%E. iApply (wp_step_fupd with "[Hshr Hα2β]");
@@ -267,13 +270,13 @@ Section code.
     iMod ("Hclose3" with "Hβ HL") as "HL".
     iMod ("Hclose2" with "H↦") as "Hα1".
     iMod ("Hclose1" with "[$] HL") as "HL".
-    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "%"; [solve_typing..|].
     (* Switch back to typing mode. *)
     iApply (type_type _ _ _ [ g ◁ own_ptr _ _; #lm +ₗ #1 ◁ &shr{α} ty ]
         with "[] LFT HE Hna HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       unlock. iFrame. iApply ty_shr_mono; last done.
-      iApply lft_incl_glb; last by iApply lft_incl_refl. done. }
+      iApply lft_incl_glb; last by iApply lft_incl_refl. by iApply lft_incl_syn_sem. }
     iApply type_letalloc_1; [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -293,7 +296,7 @@ Section code.
       iIntros (α ϝ ret arg). inv_vec arg=>g. simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (m); simpl_subst.
     (* Switch to Iris. *)
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hg [Hm _]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hg [Hm _]]".
     rewrite !tctx_hasty_val [[g]]lock /=.
     destruct m as [[|lm|]|]; try done. iDestruct "Hm" as (β) "(#Hαβ & #Hshr & Hcnt)".
     (* All right, we are done preparing our context. Let's get going. *)
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 4a1a153e61804ea31cdf73ac51eecf361644df81..5ced33ac1bdb1962d8504be05db3d1b2a3c9ba72 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -32,8 +32,8 @@ Section option.
     typed_val
       option_as_mut (fn(∀ α, ∅; &uniq{α} (option τ)) → option (&uniq{α}τ)).
   Proof.
-    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
-      inv_vec p=>o. simpl_subst.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    iIntros (α ϝ ret p). inv_vec p=>o. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (o'). simpl_subst.
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [o ◁ _; r ◁ _])) ; [solve_typing..| |].
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index f6a6b094f87a94a6605e424d6cdb27f7ab83d584..7190f6cc1ce97ce884c6b7576c3286486128970f 100644
--- a/theories/typing/lib/panic.v
+++ b/theories/typing/lib/panic.v
@@ -19,7 +19,7 @@ Section panic.
   Lemma panic_type : typed_val panic (fn(∅) → ∅).
   Proof.
     intros E L. iApply type_fn; [done|]. iIntros "!# *".
-    inv_vec args.  iIntros (tid) "LFT HE Hna HL Hk HT /=". simpl_subst.
+    inv_vec args. iIntros (tid qmax) "LFT HE Hna HL Hk HT /=". simpl_subst.
     by iApply wp_value.
   Qed.
 End panic.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 863d659cbd38db3a086738e75b1cc89f0eff537a..6f0494edf54b56d7e7d6937229a45b6ec6168915 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -227,7 +227,7 @@ Section rc.
   Global Instance rc_mono E L :
     Proper (subtype E L ==> subtype E L) rc.
   Proof.
-    iIntros (ty1 ty2 Hsub ?) "HL". iDestruct (Hsub with "HL") as "#Hsub".
+    iIntros (ty1 ty2 Hsub ??) "HL". iDestruct (Hsub with "HL") as "#Hsub".
     iIntros "!# #HE". iApply rc_subtype. by iApply "Hsub".
   Qed.
   Global Instance rc_proper E L :
@@ -398,7 +398,7 @@ Section code.
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     (* All right, we are done preparing our context. Let's get going. *)
@@ -457,7 +457,7 @@ Section code.
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     (* All right, we are done preparing our context. Let's get going. *)
@@ -517,7 +517,7 @@ Section code.
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_new (2 + ty.(ty_size))); [solve_typing..|]; iIntros (rcbox); simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (rc); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hrc [Hrcbox [Hx _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrc [Hrcbox [Hx _]]]".
     rewrite !tctx_hasty_val.
     iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
     iDestruct (ownptr_uninit_own with "Hrcbox")
@@ -560,7 +560,7 @@ Section code.
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[x]]lock.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
@@ -622,7 +622,7 @@ Section code.
       iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (x); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [#Hrc' [Hx _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrcx [#Hrc' [Hx _]]]".
     rewrite !tctx_hasty_val [[rcx]]lock.
     iDestruct (ownptr_uninit_own with "Hx") as (lrc2 vlrc2) "(% & Hx & Hx†)".
     subst x. inv_vec vlrc2=>?. rewrite heap_mapsto_vec_singleton.
@@ -692,7 +692,7 @@ Section code.
       iApply type_jump; solve_typing. }
     iIntros (k). simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock.
     destruct rc' as [[|rc'|]|]; try done.
     rewrite [[ #rc' ]]lock. wp_op. rewrite shift_loc_0 -(lock [ #rc' ]).
@@ -787,7 +787,7 @@ Section code.
       iApply type_jump; solve_typing. }
     iIntros (k). simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock.
     destruct rc' as [[|rc'|]|]; try done. rewrite [[ #rc' ]]lock.
     wp_op. rewrite shift_loc_0. rewrite -(lock [ #rc' ]).
@@ -877,7 +877,7 @@ Section code.
       iApply type_jump; solve_typing. }
     iIntros (k). simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val  [[rcx]]lock [[r]]lock.
     destruct rc' as [[|rc'|]|]; try done.
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & HL & Hclose1)"; [solve_typing..|].
@@ -1009,7 +1009,7 @@ Section code.
       iApply type_jump; solve_typing. }
     iIntros (k). simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock.
     destruct rc' as [[|rc'|]|]; try done.
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)";
@@ -1085,7 +1085,7 @@ Section code.
       iDestruct "Hty" as (ty') "#(Hty'ty & Hinv & Hs & Hν†)".
       iDestruct "Hs" as "[Hs|Hν']"; last by iDestruct (lft_tok_dead with "Hν Hν'") as "[]".
       wp_bind (of_val clone). iApply (wp_wand with "[Hna]").
-      { iApply (Hclone _ [] with "LFT HE Hna").
+      { iApply (Hclone _ [] $! _ 1%Qp with "LFT HE Hna").
           by rewrite /llctx_interp. by rewrite /tctx_interp. }
       clear clone Hclone. iIntros (clone) "(Hna & _ & Hclone)".
       wp_let. wp_let. rewrite tctx_interp_singleton tctx_hasty_val.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 91b5c4e0f08eeb68925c963d92be0e67b78fedf1..83042cbf719d6891e68775412077df2f4fe66a10 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -94,7 +94,7 @@ Section weak.
   Global Instance weak_mono E L :
     Proper (subtype E L ==> subtype E L) weak.
   Proof.
-    iIntros (ty1 ty2 Hsub ?) "HL". iDestruct (Hsub with "HL") as "#Hsub".
+    iIntros (ty1 ty2 Hsub ??) "HL". iDestruct (Hsub with "HL") as "#Hsub".
     iIntros "!# #HE". iApply weak_subtype. iApply "Hsub"; done.
   Qed.
   Global Instance weak_proper E L :
@@ -136,7 +136,7 @@ Section code.
       iApply type_jump; solve_typing. }
     iIntros (k). simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (w'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hw [Hw' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hw [Hw' [Hr _]]]".
     rewrite !tctx_hasty_val [[w]]lock.
     destruct w' as [[|lw|]|]; try done. iDestruct "Hw'" as (l') "[#Hlw #Hshr]".
     iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
@@ -238,7 +238,7 @@ Section code.
     iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[x]]lock.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
@@ -301,7 +301,7 @@ Section code.
     iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[x]]lock.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
@@ -383,7 +383,7 @@ Section code.
       iApply type_jump; solve_typing. }
     iIntros (k). simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (w'); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hw [Hw' _]]".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hw [Hw' _]]".
     rewrite !tctx_hasty_val [[w]]lock. destruct w' as [[|lw|]|]; try done. wp_op.
     iDestruct "Hw'" as (γ ν) "[#Hpersist Hwtok]".
     iAssert (∃ wv : Z, (lw +ₗ 1) ↦ #wv ∗
@@ -452,7 +452,7 @@ Section code.
       iIntros (_ ϝ ret arg). inv_vec arg. simpl_subst.
     iApply (type_new (2 + ty.(ty_size))); [solve_typing..|]; iIntros (rcbox); simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (w); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hw [Hrcbox _]]". rewrite !tctx_hasty_val.
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hw [Hrcbox _]]". rewrite !tctx_hasty_val.
     iDestruct (ownptr_uninit_own with "Hrcbox") as (lrcbox vlrcbox)
        "(% & Hrcbox↦ & Hrcbox†)". subst rcbox. inv_vec vlrcbox=>??? /=.
     iDestruct (heap_mapsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index 87cd76a52c6cafb6409a414288fa16dfef187591..f50312d3ffde3f4456b0004573672a436ffe60e0 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -80,22 +80,22 @@ Section ref.
   Global Instance ref_mono E L :
     Proper (flip (lctx_lft_incl E L) ==> subtype E L ==> subtype E L) ref.
   Proof.
-    iIntros (α1 α2 Hα ty1 ty2 Hty q) "HL".
+    iIntros (α1 α2 Hα ty1 ty2 Hty qmax qL) "HL".
     iDestruct (Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
-    iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
+    iIntros "!# #HE". iDestruct ("Hα" with "HE") as %Hα1α2.
     iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
     - done.
     - iIntros (tid [|[[]|][|[[]|][]]]) "H"=>//=.
       iDestruct "H" as (ν q' γ β ty') "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
       iExists ν, q', γ, β, ty'. iFrame "∗#". iSplit.
       + iApply ty_shr_mono; last by iApply "Hs".
-        iApply lft_intersect_mono. done. iApply lft_incl_refl.
-      + by iApply lft_incl_trans.
+        iApply lft_intersect_mono; first by iApply lft_incl_syn_sem. iApply lft_incl_refl.
+      + iApply lft_incl_trans; first by iApply lft_incl_syn_sem. done.
     - iIntros (κ tid l) "H /=". iDestruct "H" as (ν q' γ β ty' lv lrc) "H".
       iExists ν, q', γ, β, ty', lv, lrc. iDestruct "H" as "#($&$&?&?&$&$)". iSplit.
       + iApply ty_shr_mono; last by iApply "Hs".
-        iApply lft_intersect_mono. done. iApply lft_incl_refl.
-      + by iApply lft_incl_trans.
+        iApply lft_intersect_mono; first by iApply lft_incl_syn_sem. iApply lft_incl_refl.
+      + iApply lft_incl_trans; first by iApply lft_incl_syn_sem. done.
   Qed.
   Global Instance ref_mono_flip E L :
     Proper (lctx_lft_incl E L ==> flip (subtype E L) ==> flip (subtype E L)) ref.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 27baff9cf46b087c43ceb286d4e5ee6d12dd182d..f279e518c1b6a3b4c8017d0968984fe501e86df7 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -51,14 +51,14 @@ Section ref_functions.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
-    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    iIntros (tid qmax) "#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'|]|]=>//=.
     iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hβδ & Hinv & H◯inv)".
     wp_op.
     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.
-    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose')";
+    iMod (lctx_lft_alive_tok_noend α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose')";
       [solve_typing..|].
     iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
     iMod (na_bor_acc with "LFT Hinv Hδ Hna") as "(INV & Hna & Hcloseδ)"; [done..|].
@@ -111,7 +111,7 @@ Section ref_functions.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
-    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    iIntros (tid qmax) "#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'|]|]=>//=.
     iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hx')".
@@ -120,12 +120,13 @@ Section ref_functions.
     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..|].
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as %?; [solve_typing..|].
     iApply (type_type _ _ _
         [ x ◁ box (&shr{α}(ref β ty)); #lv ◁ &shr{α}ty]
         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"). by iApply lft_incl_glb. }
+      iFrame. iApply (ty_shr_mono with "[] Hshr").
+      iApply lft_incl_glb; last done. by iApply lft_incl_syn_sem. }
     iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -146,7 +147,7 @@ Section ref_functions.
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk Hx". rewrite tctx_interp_singleton tctx_hasty_val.
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk Hx". rewrite tctx_interp_singleton tctx_hasty_val.
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
     iDestruct "Hx" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hx"; simpl;
       try iDestruct "Hx" as "[_ >[]]".
@@ -209,10 +210,11 @@ Section ref_functions.
     typed_val call_once (fn(∀ α, ∅; fty, &shr{α}ty1) → &shr{α}ty2) →
     typed_val (ref_map call_once) (fn(∀ α, ∅; ref α ty1, fty) → ref α ty2).
   Proof.
-    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
+    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    iIntros (α ϝ ret arg).
        inv_vec arg=>ref env. simpl_subst.
     iApply type_let; [apply Hf | solve_typing |]. iIntros (f'). simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk (#Hf' & Href & Henv & _)".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk (#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"; simpl;
@@ -224,10 +226,10 @@ Section ref_functions.
     iIntros (lx) "(H† & Hlx)". rewrite heap_mapsto_vec_singleton.
     wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
     iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
-    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
+    iMod (lctx_lft_alive_tok_noend ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
     iDestruct (lft_intersect_acc with "Hα Hν") as (?) "[Hαν Hclose3]".
     iDestruct (lft_intersect_acc with "Hαν Hϝ") as (?) "[Hανϝ Hclose4]".
-    rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ](right_id_L).
+    rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ]right_id_L.
     iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) [_; _]
        with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H†]"); [solve_typing|done| |].
     { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
@@ -287,10 +289,11 @@ Section ref_functions.
     typed_val (ref_map_split call_once)
               (fn(∀ α, ∅; ref α ty, fty) → Π[ref α ty1; ref α ty2]).
   Proof.
-    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
+    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    iIntros (α ϝ ret arg).
        inv_vec arg=>ref env. simpl_subst.
     iApply type_let; [apply Hf | solve_typing |]. iIntros (f'). simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk (#Hf' & Href & Henv & _)".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk (#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"; simpl;
@@ -302,10 +305,10 @@ Section ref_functions.
     iIntros (lx) "(H† & Hlx)". rewrite heap_mapsto_vec_singleton.
     wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
     iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
-    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
+    iMod (lctx_lft_alive_tok_noend ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
     iDestruct (lft_intersect_acc with "Hα Hν") as (?) "[Hαν Hclose3]".
     iDestruct (lft_intersect_acc with "Hαν Hϝ") as (?) "[Hανϝ Hclose4]".
-    rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ](right_id_L).
+    rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ]right_id_L.
     iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) [_; _]
        with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H†]"); [solve_typing|done| |].
     { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index bb8b21c58e8c600124521e7002da6dc4a62e4a9e..b089b73dc9bbba32869667a817ebb4a78d442894 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -68,9 +68,9 @@ Section refcell_inv.
     eapply refcell_inv_type_ne, type_dist_dist2. done.
   Qed.
 
-  Lemma refcell_inv_proper E L ty1 ty2 q :
+  Lemma refcell_inv_proper E L ty1 ty2 qmax qL :
     eqtype E L ty1 ty2 →
-    llctx_interp L q -∗ ∀ tid l γ α, □ (elctx_interp E -∗
+    llctx_interp_noend qmax L qL -∗ ∀ tid l γ α, □ (elctx_interp E -∗
     refcell_inv tid l γ α ty1 -∗ refcell_inv tid l γ α ty2).
   Proof.
     (* TODO : this proof is essentially [solve_proper], but within the logic. *)
@@ -183,7 +183,7 @@ Section refcell.
   Proof.
     (* TODO : this proof is essentially [solve_proper], but within the logic.
               It would easily gain from some automation. *)
-    iIntros (ty1 ty2 EQ qL) "HL". generalize EQ. rewrite eqtype_unfold=>EQ'.
+    iIntros (ty1 ty2 EQ qmax qL) "HL". generalize EQ. rewrite eqtype_unfold=>EQ'.
     iDestruct (EQ' with "HL") as "#EQ'".
     iDestruct (refcell_inv_proper with "HL") as "#Hty1ty2"; first done.
     iDestruct (refcell_inv_proper with "HL") as "#Hty2ty1"; first by symmetry.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 85f3629e69b8843ae2280670e6fb549f1cf0b6b6..c494d48579262addecf8362f7ee3d180fa93a5f9 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -24,7 +24,7 @@ Section refcell_functions.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_new (S ty.(ty_size))); [solve_typing..|].
-    iIntros (r tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    iIntros (r tid qmax) "#LFT #HE Hna HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hr Hx]".
     iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
@@ -58,7 +58,7 @@ Section refcell_functions.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_new ty.(ty_size)); [solve_typing..|].
-    iIntros (r tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    iIntros (r tid qmax) "#LFT #HE Hna HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hr Hx]".
     iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & >Hx↦ & Hx & Hx†)". subst x.
@@ -91,7 +91,7 @@ Section refcell_functions.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL HC HT".
+    iIntros (tid qmax) "#LFT #HE Hna HL HC HT".
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|];  try iDestruct "Hx'" as "[]".
     iAssert (&{α} (∃ (z : Z), lx' ↦ #z) ∗
@@ -149,7 +149,7 @@ Section refcell_functions.
     { iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing. }
     iApply type_deref; [solve_typing..|].
-    iIntros (x' tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    iIntros (x' tid qmax) "#LFT #HE Hna HL Hk HT". simpl_subst.
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]=>//=.
     iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
@@ -259,7 +259,7 @@ Section refcell_functions.
     { iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing. }
     iApply type_deref; [solve_typing..|].
-    iIntros (x' tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    iIntros (x' tid qmax) "#LFT #HE Hna HL Hk HT". simpl_subst.
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]=>//=.
     iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 8d2978ff505c66dcc2b01c0b6312c65314418582..3da42ad70231601cce3089d7a29ebf7058d26902 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -85,27 +85,29 @@ Section refmut.
   Global Instance refmut_mono E L :
     Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) refmut.
   Proof.
-    intros α1 α2 Hα ty1 ty2. rewrite eqtype_unfold=>Hty. iIntros (q) "HL".
+    intros α1 α2 Hα ty1 ty2. rewrite eqtype_unfold=>Hty. iIntros (qmax qL) "HL".
     iDestruct (Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
-    iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
+    iIntros "!# #HE". iDestruct ("Hα" with "HE") as %Hα1α2.
     iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
     - done.
     - iIntros (tid [|[[]|][|[[]|][]]]) "H"=>//=.
       iDestruct "H" as (ν γ q' β ty') "(Hb & #H⊑ & #Hinv & Hν & Hown)".
       iExists ν, γ, q', β, ty'. iFrame "∗#". iSplit.
       + iApply bor_shorten; last iApply bor_iff; last done.
-        * iApply lft_intersect_mono; first done. iApply lft_incl_refl.
+        * iApply lft_intersect_mono; first by iApply lft_incl_syn_sem.
+          iApply lft_incl_refl.
         * iNext; iModIntro; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
           iExists vl; iFrame; by iApply "Ho".
-      + by iApply lft_incl_trans.
+      + iApply lft_incl_trans; last done. by iApply lft_incl_syn_sem.
     - iIntros (κ tid l) "H /=". iDestruct "H" as (lv lrc) "H". iExists lv, lrc.
       iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
       iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
-      { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
-      iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
+      { iApply lft_intersect_mono; first by iApply lft_incl_syn_sem. iApply lft_incl_refl. }
+      iMod ("H" with "[] Htok") as "Hshr"; first done. iModIntro. iNext.
       iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
-      iApply ty_shr_mono; try done. iApply lft_intersect_mono. done. iApply lft_incl_refl.
-      by iApply "Hs".
+      iApply ty_shr_mono; try done.
+      + iApply lft_intersect_mono. by iApply lft_incl_syn_sem. iApply lft_incl_refl.
+      + by iApply "Hs".
   Qed.
   Global Instance refmut_mono_flip E L :
     Proper (lctx_lft_incl E L ==> eqtype E L ==> flip (subtype E L)) refmut.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 2a32ac07d8274fca8e109f37b5cf78c8e20da255..23e1ce165dfef82f1f78c149aef0f0c4286a896c 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -23,7 +23,7 @@ Section refmut_functions.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
-    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    iIntros (tid qmax) "#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'|]|]=>//=.
     iDestruct "Hx'" as (lv lrc) "#(Hfrac & #Hshr)".
@@ -31,7 +31,7 @@ Section refmut_functions.
       [solve_typing..|].
     iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
     rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
-    iMod (lctx_lft_alive_tok β with "HE HL") as (qβ) "(Hβ & HL & Hclose'')";
+    iMod (lctx_lft_alive_tok_noend β with "HE HL") as (qβ) "(Hβ & HL & Hclose'')";
       [solve_typing..|].
     iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
     wp_bind (!#lx')%E. iApply (wp_step_fupd with "[Hα2β]");
@@ -40,12 +40,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..|].
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as %?; [solve_typing..|].
     iApply (type_type _ _ _ [ x ◁ box (&shr{α}(refmut β ty)); #lv ◁ &shr{α}ty]
             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'").
-      by iApply lft_incl_glb; last iApply lft_incl_refl. }
+      iApply lft_incl_glb; last iApply lft_incl_refl. by iApply lft_incl_syn_sem. }
     iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -61,7 +61,7 @@ Section refmut_functions.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
-    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    iIntros (tid qmax) "#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.
     iMod (bor_exists with "LFT Hx'") as (vl) "H". done.
@@ -88,12 +88,13 @@ Section refmut_functions.
     wp_bind (!#lx')%E. iMod (bor_unnest with "LFT Hb") as "Hb"; first done.
     wp_read. wp_let. iMod "Hb".
     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..|].
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as %?; [solve_typing..|].
     iApply (type_type _ _ _ [ x ◁ box (uninit 1); #lv ◁ &uniq{α}ty]
             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").
-      by iApply lft_incl_glb; [iApply lft_incl_glb|iApply lft_incl_refl]. }
+        iApply lft_incl_glb; [iApply lft_incl_glb|iApply lft_incl_refl];
+          try by iApply lft_incl_syn_sem. done. }
     iApply (type_letalloc_1 (&uniq{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -114,7 +115,7 @@ Section refmut_functions.
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk Hx". rewrite tctx_interp_singleton tctx_hasty_val.
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk Hx". rewrite tctx_interp_singleton tctx_hasty_val.
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
     iDestruct "Hx" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hx"; simpl;
       try iDestruct "Hx" as "[_ >[]]".
@@ -180,10 +181,11 @@ Section refmut_functions.
     typed_val call_once (fn(∀ α, ∅; fty, &uniq{α}ty1) → &uniq{α}ty2) →
     typed_val (refmut_map call_once) (fn(∀ α, ∅; refmut α ty1, fty) → refmut α ty2).
   Proof.
-    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
+    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    iIntros (α ϝ ret arg).
        inv_vec arg=>ref env. simpl_subst.
     iApply type_let; [apply Hf | solve_typing |]. iIntros (f'). simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk (#Hf' & Href & Henv & _)".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk (#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"; simpl;
@@ -195,7 +197,7 @@ Section refmut_functions.
     iIntros (lx) "(H† & Hlx)". rewrite heap_mapsto_vec_singleton.
     wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
     iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
-    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
+    iMod (lctx_lft_alive_tok_noend ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
     iDestruct (lft_intersect_acc with "Hα Hν") as (?) "[Hαν Hclose3]".
     iDestruct (lft_intersect_acc with "Hαν Hϝ") as (?) "[Hανϝ Hclose4]".
     rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ](right_id_L).
@@ -258,10 +260,11 @@ Section refmut_functions.
     typed_val (refmut_map_split call_once)
               (fn(∀ α, ∅; refmut α ty, fty) → Π[refmut α ty1; refmut α ty2]).
   Proof.
-    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
+    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    iIntros (α ϝ ret arg).
        inv_vec arg=>refmut env. simpl_subst.
     iApply type_let; [apply Hf | solve_typing |]. iIntros (f'). simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk (#Hf' & Hrefmut & Henv & _)".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk (#Hf' & Hrefmut & Henv & _)".
     rewrite (tctx_hasty_val _ refmut). destruct refmut as [[|lrefmut|]|]; try done.
     iDestruct "Hrefmut" as "[Hrefmut Hrefmut†]".
     iDestruct "Hrefmut" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hrefmut"; simpl;
@@ -273,10 +276,10 @@ Section refmut_functions.
     iIntros (lx) "(H† & Hlx)". rewrite heap_mapsto_vec_singleton.
     wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
     iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
-    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
+    iMod (lctx_lft_alive_tok_noend ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
     iDestruct (lft_intersect_acc with "Hα Hν") as (?) "[Hαν Hclose3]".
     iDestruct (lft_intersect_acc with "Hαν Hϝ") as (?) "[Hανϝ Hclose4]".
-    rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ](right_id_L).
+    rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ]right_id_L.
     iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) [_; _]
        with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H† Hbor]"); [solve_typing|done| |].
     { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index b4923b117d7ce82f40315b483c2387bd3c1f726e..889ec4d10df8783ac1b0b0aa3589f7bdf4fbfae3 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -60,9 +60,9 @@ Section rwlock_inv.
     intros n ???. eapply rwlock_inv_type_ne, type_dist_dist2. done.
   Qed.
 
-  Lemma rwlock_inv_proper E L ty1 ty2 q :
+  Lemma rwlock_inv_proper E L ty1 ty2 qmax qL :
     eqtype E L ty1 ty2 →
-    llctx_interp L q -∗ ∀ tid_own tid_shr l γ α, □ (elctx_interp E -∗
+    llctx_interp_noend qmax L qL -∗ ∀ tid_own tid_shr l γ α, □ (elctx_interp E -∗
     rwlock_inv tid_own tid_shr l γ α ty1 -∗
     rwlock_inv tid_own tid_shr l γ α ty2).
   Proof.
@@ -190,7 +190,7 @@ Section rwlock.
   Proof.
     (* TODO : this proof is essentially [solve_proper], but within the logic.
               It would easily gain from some automation. *)
-    iIntros (ty1 ty2 EQ qL) "HL". generalize EQ. rewrite eqtype_unfold=>EQ'.
+    iIntros (ty1 ty2 EQ qmax qL) "HL". generalize EQ. rewrite eqtype_unfold=>EQ'.
     iDestruct (EQ' with "HL") as "#EQ'".
     iDestruct (rwlock_inv_proper with "HL") as "#Hty1ty2"; first done.
     iDestruct (rwlock_inv_proper with "HL") as "#Hty2ty1"; first by symmetry.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 175cf68c9ba825498a1b34008232c79be14585f5..41bd404c478ba7ee29306de92daeb981bc582825 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -24,7 +24,7 @@ Section rwlock_functions.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_new (S ty.(ty_size))); [solve_typing..|].
-    iIntros (r tid) "#LFT HE Hna HL Hk HT". simpl_subst.
+    iIntros (r tid qmax) "#LFT HE Hna HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try done.
     iDestruct "Hx" as "[Hx Hx†]". iDestruct "Hx" as (vl) "[Hx↦ Hx]".
@@ -59,7 +59,7 @@ Section rwlock_functions.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_new ty.(ty_size)); [solve_typing..|].
-    iIntros (r tid) "#LFT HE Hna HL Hk HT". simpl_subst.
+    iIntros (r tid qmax) "#LFT HE Hna HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try done.
     iDestruct "Hx" as "[Hx Hx†]".
@@ -92,7 +92,7 @@ Section rwlock_functions.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
-    iIntros (tid) "#LFT HE Hna HL HC HT".
+    iIntros (tid qmax) "#LFT HE Hna HL HC HT".
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|];  try iDestruct "Hx'" as "[]".
     iAssert (&{α} (∃ (z : Z), lx' ↦ #z ∗ ⌜-1 ≤ z⌝) ∗
@@ -154,7 +154,7 @@ Section rwlock_functions.
       [iIntros (loop)|iIntros "/= !#"; iIntros (loop arg); inv_vec arg];
       simpl_subst.
     { iApply type_jump; solve_typing. }
-    iIntros (tid) "#LFT #HE Hna HL Hk HT".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk HT".
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
     iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
@@ -262,7 +262,7 @@ Section rwlock_functions.
     { iApply type_delete; [solve_typing..|]. iApply type_jump; solve_typing. }
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_deref; [solve_typing..|].
-    iIntros (x' tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    iIntros (x' tid qmax) "#LFT #HE Hna HL Hk HT". simpl_subst.
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
     iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index f3d6ac7841c3ba1b61c0f58d64f4b535fb8adb50..e33822fca1e791204c7df40d073b37ae07097274 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -79,24 +79,24 @@ Section rwlockreadguard.
   Global Instance rwlockreadguard_mono E L :
     Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) rwlockreadguard.
   Proof.
-    iIntros (α1 α2 Hα ty1 ty2 Hty q) "HL".
+    iIntros (α1 α2 Hα ty1 ty2 Hty qmax qL) "HL".
     iDestruct (proj1 Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
     iDestruct (rwlock_inv_proper with "HL") as "#Hty1ty2"; first done.
     iDestruct (rwlock_inv_proper with "HL") as "#Hty2ty1"; first by symmetry.
-    iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
+    iIntros "!# #HE". iDestruct ("Hα" with "HE") as %Hα1α2.
     iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
     - done.
     - iIntros (tid [|[[]|][]]) "H"; try done.
       iDestruct "H" as (ν q' γ β tid_own) "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
       iExists ν, q', γ, β, tid_own. iFrame "∗#". iSplit; last iSplit.
       + iApply ty_shr_mono; last by iApply "Hs".
-        iApply lft_intersect_mono. done. iApply lft_incl_refl.
-      + by iApply lft_incl_trans.
+        iApply lft_intersect_mono; first by iApply lft_incl_syn_sem. iApply lft_incl_refl.
+      + iApply lft_incl_trans; first by iApply lft_incl_syn_sem. done.
       + iApply (at_bor_iff with "[] Hinv").
         iIntros "!> !#"; iSplit; iIntros "H". by iApply "Hty1ty2". by iApply "Hty2ty1".
     - iIntros (κ tid l) "H". iDestruct "H" as (l') "[Hf Hshr]". iExists l'.
       iFrame. iApply ty_shr_mono; last by iApply "Hs".
-      iApply lft_intersect_mono. done. iApply lft_incl_refl.
+      iApply lft_intersect_mono; first by iApply lft_incl_syn_sem. iApply lft_incl_refl.
   Qed.
   Global Instance rwlockreadguard_mono_flip E L :
     Proper (lctx_lft_incl E L ==> eqtype E L ==> flip (subtype E L))
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 20c1ab6ce8ff1630ccf38cd0979c4579519ba37b..f6dccc46beeca9fe1b78d21f58b4df108e203bc3 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -24,7 +24,7 @@ Section rwlockreadguard_functions.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
-    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    iIntros (tid qmax) "#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.
     iDestruct "Hx'" as (l') "#[Hfrac Hshr]".
@@ -32,12 +32,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..|].
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as %?; [solve_typing..|].
     iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rwlockreadguard β ty));
                               #(l' +ₗ 1) ◁ &shr{α}ty]
       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; first done.
+      iFrame. iApply (ty_shr_mono with "[] Hshr").
+      iApply lft_incl_glb; first by iApply lft_incl_syn_sem.
       by iApply lft_incl_refl. }
     iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
@@ -67,7 +68,7 @@ Section rwlockreadguard_functions.
       [iIntros (loop)|iIntros "/= !#"; iIntros (loop arg); inv_vec arg];
       simpl_subst.
     { iApply type_jump; solve_typing. }
-    iIntros (tid) "#LFT #HE Hna HL Hk HT".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk HT".
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']".
     destruct x' as [[|lx'|]|]; try done. simpl.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 8b5666b389ac56883a527016131f950412d054ed..0342b547b83b9f522a084f2ae69810ece28a3d39 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -77,11 +77,12 @@ Section rwlockwriteguard.
   Global Instance rwlockwriteguard_mono E L :
     Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) rwlockwriteguard.
   Proof.
-    intros α1 α2 Hα ty1 ty2 Hty. generalize Hty. rewrite eqtype_unfold. iIntros (Hty' q) "HL".
+    intros α1 α2 Hα ty1 ty2 Hty. generalize Hty. rewrite eqtype_unfold.
+    iIntros (Hty' qmax qL) "HL".
     iDestruct (Hty' with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
     iDestruct (rwlock_inv_proper with "HL") as "#Hty1ty2"; first done.
     iDestruct (rwlock_inv_proper with "HL") as "#Hty2ty1"; first by symmetry.
-    iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
+    iIntros "!# #HE". iDestruct ("Hα" with "HE") as %Hα1α2.
     iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
     - done.
     - iIntros (tid [|[[]|][]]) "H"; try done.
@@ -90,17 +91,18 @@ Section rwlockwriteguard.
       + iApply bor_iff; last done.
         iNext; iModIntro; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
         iExists vl; iFrame; by iApply "Ho".
-      + by iApply lft_incl_trans.
+      + iApply lft_incl_trans; first by iApply lft_incl_syn_sem. done.
       + iApply at_bor_iff; try done.
         iIntros "!>!#"; iSplit; iIntros "H". by iApply "Hty1ty2". by iApply "Hty2ty1".
     - iIntros (κ tid l) "H". iDestruct "H" as (l') "H". iExists l'.
       iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
       iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
-      { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
-      iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
+      { iApply lft_intersect_mono; first by iApply lft_incl_syn_sem. iApply lft_incl_refl. }
+      iMod ("H" with "[] Htok") as "Hshr"; first done. iModIntro. iNext.
       iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
-      iApply ty_shr_mono; try done. iApply lft_intersect_mono. done. iApply lft_incl_refl.
-      by iApply "Hs".
+      iApply ty_shr_mono; try done.
+      + iApply lft_intersect_mono; first by iApply lft_incl_syn_sem. iApply lft_incl_refl.
+      + by iApply "Hs".
   Qed.
   Global Instance rwlockwriteguard_mono_flip E L :
     Proper (lctx_lft_incl E L ==> eqtype E L ==> flip (subtype E L)) rwlockwriteguard.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 15cb2bee84480658ef3520a5cc89ceae0467e27a..9ff168868b43c22132c2452ed77ece9783af7a65 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -24,7 +24,7 @@ Section rwlockwriteguard_functions.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
-    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    iIntros (tid qmax) "#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.
     iDestruct "Hx'" as (l') "#[Hfrac Hshr]".
@@ -32,7 +32,7 @@ Section rwlockwriteguard_functions.
       [solve_typing..|].
     iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
     rewrite heap_mapsto_vec_singleton.
-    iMod (lctx_lft_alive_tok β with "HE HL") as (qβ) "(Hβ & HL & Hclose')";
+    iMod (lctx_lft_alive_tok_noend β with "HE HL") as (qβ) "(Hβ & HL & Hclose')";
       [solve_typing..|].
     iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
     wp_bind (!(LitV lx'))%E. iApply (wp_step_fupd with "[Hα2β]");
@@ -41,13 +41,14 @@ 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..|].
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as %?; [solve_typing..|].
     iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rwlockwriteguard β ty));
                               #(l' +ₗ 1) ◁ &shr{α}ty]
             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; first done.
-        by iApply lft_incl_refl. }
+      iFrame. iApply (ty_shr_mono with "[] Hshr'").
+      iApply lft_incl_glb; first by iApply lft_incl_syn_sem.
+      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.
@@ -68,7 +69,7 @@ Section rwlockwriteguard_functions.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
-    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
+    iIntros (tid qmax) "#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.
     iMod (bor_exists with "LFT Hx'") as (vl) "H". done.
@@ -87,12 +88,13 @@ Section rwlockwriteguard_functions.
     wp_bind (!(LitV lx'))%E. iMod (bor_unnest with "LFT Hb") as "Hb"; first done.
     wp_read. wp_op. wp_let. iMod "Hb".
     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..|].
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as %?; [solve_typing..|].
     iApply (type_type _ _ _ [ x ◁ box (uninit 1); #(l +ₗ 1) ◁ &uniq{α}ty]
             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. by iApply lft_incl_refl. }
+      iApply lft_incl_trans; last done. by iApply lft_incl_syn_sem.
+      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.
@@ -113,7 +115,7 @@ Section rwlockwriteguard_functions.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk HT".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk HT".
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']".
     destruct x' as [[|lx'|]|]; try done. simpl.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index f6caa8ea7339a49895aabe12a0fa3682ec9360f3..a546ad1545023ed8723656a73edf4f198697b0c8 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -42,7 +42,7 @@ Section join_handle.
   Global Instance join_handle_mono E L :
     Proper (subtype E L ==> subtype E L) join_handle.
   Proof.
-    iIntros (ty1 ty2 Hsub ?) "HL". iDestruct (Hsub with "HL") as "#Hsub".
+    iIntros (ty1 ty2 Hsub ??) "HL". iDestruct (Hsub with "HL") as "#Hsub".
     iIntros "!# #HE". iApply join_handle_subtype. iApply "Hsub"; done.
   Qed.
   Global Instance join_handle_proper E L :
@@ -88,7 +88,7 @@ Section spawn.
     iApply (type_let _ _ _ _ ([f' ◁ _; env ◁ _])
                      (λ j, [j ◁ join_handle retty])); try solve_typing; [|].
     { (* The core of the proof: showing that spawn is safe. *)
-      iIntros (tid) "#LFT #HE $ $ [Hf' [Henv _]]". rewrite !tctx_hasty_val [fn _]lock.
+      iIntros (tid qmax) "#LFT #HE $ $ [Hf' [Henv _]]". rewrite !tctx_hasty_val [fn _]lock.
       iApply (spawn_spec _ (join_inv retty) with "[-]"); last first.
       { iIntros "!> *". rewrite tctx_interp_singleton tctx_hasty_val.
         iIntros "?". by iFrame. }
@@ -121,7 +121,7 @@ Section spawn.
     iApply type_deref; [solve_typing..|]. iIntros (c'); simpl_subst.
     iApply (type_let _ _ _ _ ([c' ◁ _])
                              (λ r, [r ◁ box retty])); try solve_typing; [|].
-    { iIntros (tid) "#LFT _ $ $".
+    { iIntros (tid qmax) "#LFT _ $ $".
       rewrite tctx_interp_singleton tctx_hasty_val. iIntros "Hc".
       destruct c' as [[|c'|]|]; try done.
       iApply (join_spec with "Hc"). iNext. iIntros "* Hret".
diff --git a/theories/typing/lib/swap.v b/theories/typing/lib/swap.v
index 860b1c07be5d4633d843b8b5ed85b843e1b3eaf1..e76b730cc231e31814b042d0e224604e8603c9e7 100644
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
@@ -21,7 +21,7 @@ Section swap.
       inv_vec p=>p1 p2. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (p1'). simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (p2'). simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk (H2 & H2' & H1 & H1' & _)".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk (H2 & H2' & H1 & H1' & _)".
     rewrite !tctx_hasty_val.
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose)";
       [solve_typing..|].
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index b051af66cfa59584329e51ec01513c88e7578b6f..7acd8b79968c5b899a16077593415f6b7c9f7643 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -23,18 +23,18 @@ Section code.
     typed_val call_once (fn(∅; fty, ty) → ty) →
     typed_val (take ty call_once) (fn(∀ α, ∅; &uniq{α} ty, fty) → unit).
   Proof.
-    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
-      inv_vec arg=>x env. simpl_subst.
+    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+    iIntros (α ϝ ret arg). inv_vec arg=>x env. simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (x'); simpl_subst.
     iApply type_let; [apply Hf|solve_typing|]; iIntros (f'); simpl_subst.
     iApply (type_new ty.(ty_size)); [solve_typing..|]; iIntros (t); simpl_subst.
     (* Switch to Iris. *)
-    iIntros (tid) "#LFT #HE Hna HL Hk (Ht & Hf' & Hx & Hx' & Henv & _)".
+    iIntros (tid qmax) "#LFT #HE Hna HL Hk (Ht & Hf' & Hx & Hx' & Henv & _)".
     rewrite !tctx_hasty_val [[x]]lock [[env]]lock [fn _]lock.
     iDestruct (ownptr_uninit_own with "Ht") as (tl tvl) "(% & >Htl & Htl†)". subst t. simpl.
     destruct x' as [[|lx'|]|]; try done. simpl.
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose1)"; [solve_typing..|].
-    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (qϝ) "(Hϝ & HL & Hclose2)"; [solve_typing..|].
+    iMod (lctx_lft_alive_tok_noend ϝ with "HE HL") as (qϝ) "(Hϝ & HL & Hclose2)"; [solve_typing..|].
     iMod (bor_acc with "LFT Hx' Hα") as "[Hx' Hclose3]"; first done.
     iDestruct (heap_mapsto_ty_own with "Hx'") as (x'vl) "[>Hx'↦ Hx'vl]".
     wp_apply (wp_memcpy with "[$Htl $Hx'↦]"); [by auto using vec_to_list_length..|].
diff --git a/theories/typing/own.v b/theories/typing/own.v
index a4073bfb57ce0511c9f0334ede4b860d5165163e..3de55448c0fc7a379ae4b7055358be64d82804b0 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -106,7 +106,7 @@ Section own.
   Global Instance own_mono E L n :
     Proper (subtype E L ==> subtype E L) (own_ptr n).
   Proof.
-    intros ty1 ty2 Hincl. iIntros (qL) "HL".
+    intros ty1 ty2 Hincl. iIntros (qmax qL) "HL".
     iDestruct (Hincl with "HL") as "#Hincl".
     iClear "∗". iIntros "!# #HE".
     iApply own_type_incl; first by auto. iApply "Hincl"; auto.
@@ -160,7 +160,7 @@ Section box.
   Global Instance box_mono E L :
     Proper (subtype E L ==> subtype E L) box.
   Proof.
-    intros ty1 ty2 Hincl. iIntros (qL) "HL".
+    intros ty1 ty2 Hincl. iIntros (qmax qL) "HL".
     iDestruct (Hincl with "HL") as "#Hincl".
     iClear "∗". iIntros "!# #HE".
     iApply box_type_incl. iApply "Hincl"; auto.
@@ -221,7 +221,7 @@ Section typing.
     ty.(ty_size) = ty'.(ty_size) → ⊢ typed_write E L (own_ptr n ty') ty (own_ptr n ty).
   Proof.
     rewrite typed_write_eq. iIntros (Hsz) "!#".
-    iIntros ([[]|] tid F qL ?) "_ _ $ Hown"; try done.
+    iIntros ([[]|] tid F qmax qL ?) "_ _ $ Hown"; try done.
     rewrite /= Hsz. iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iDestruct (ty_size_eq with "Hown") as "#>%". iExists _, _. iFrame "H↦". auto.
   Qed.
@@ -230,7 +230,7 @@ Section typing.
     Copy ty → ⊢ typed_read E L (own_ptr n ty) ty (own_ptr n ty).
   Proof.
     rewrite typed_read_eq. iIntros (Hsz) "!#".
-    iIntros ([[]|] tid F qL ?) "_ _ $ $ Hown"; try done.
+    iIntros ([[]|] tid F qmax qL ?) "_ _ $ $ Hown"; try done.
     iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iExists l, _, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !>".
     iExists _. auto.
@@ -240,7 +240,7 @@ Section typing.
     ⊢ typed_read E L (own_ptr n ty) ty (own_ptr n $ uninit ty.(ty_size)).
   Proof.
     rewrite typed_read_eq. iModIntro.
-    iIntros ([[]|] tid F qL ?) "_ _ $ $ Hown"; try done.
+    iIntros ([[]|] tid F qmax qL ?) "_ _ $ $ Hown"; try done.
     iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iDestruct (ty_size_eq with "Hown") as "#>%".
     iExists l, vl, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !> !>".
@@ -252,7 +252,7 @@ Section typing.
     ⊢ let n' := Z.to_nat n in
       typed_instruction_ty E L [] (new [ #n ]%E) (own_ptr n' (uninit n')).
   Proof.
-    iIntros (? tid) "#LFT #HE $ $ _".
+    iIntros (? tid qmax) "#LFT #HE $ $ _".
     iApply wp_new; try done. iModIntro.
     iIntros (l) "(H† & Hlft)". rewrite tctx_interp_singleton tctx_hasty_val.
     iNext. rewrite freeable_sz_full Z2Nat.id //. iFrame.
@@ -285,7 +285,7 @@ Section typing.
     Z.of_nat (ty.(ty_size)) = n →
     ⊢ typed_instruction E L [p ◁ own_ptr ty.(ty_size) ty] (delete [ #n; p])%E (λ _, []).
   Proof.
-    iIntros (<- tid) "#LFT #HE $ $ Hp". rewrite tctx_interp_singleton.
+    iIntros (<- tid qmax) "#LFT #HE $ $ Hp". rewrite tctx_interp_singleton.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
     iDestruct "Hown" as "[H↦: >H†]". iDestruct "H↦:" as (vl) "[>H↦ Hown]".
     iDestruct (ty_size_eq with "Hown") as "#>EQ".
diff --git a/theories/typing/product.v b/theories/typing/product.v
index c0e28c9bcb6e4a3f1016e3195a0f336baf888e81..d1d5b103a0e320b3a0c790753e06fab25f1d3bbc 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -89,7 +89,7 @@ Section product.
   Global Instance product2_mono E L:
     Proper (subtype E L ==> subtype E L ==> subtype E L) product2.
   Proof.
-    iIntros (ty11 ty12 H1 ty21 ty22 H2). iIntros (qL) "HL".
+    iIntros (ty11 ty12 H1 ty21 ty22 H2). iIntros (qmax qL) "HL".
     iDestruct (H1 with "HL") as "#H1". iDestruct (H2 with "HL") as "#H2".
     iClear "∗". iIntros "!# #HE".
     iDestruct ("H1" with "HE") as "#(% & #Ho1 & #Hs1)". clear H1.
@@ -199,7 +199,7 @@ Section typing.
 
   Global Instance prod2_assoc E L : Assoc (eqtype E L) product2.
   Proof.
-    intros ???. apply eqtype_unfold. iIntros (?) "_ !# _".
+    intros ???. apply eqtype_unfold. iIntros (??) "_ !# _".
     iSplit; first by rewrite /= assoc. iSplit; iIntros "!# *"; iSplit; iIntros "H".
     - iDestruct "H" as (vl1 vl') "(% & Ho1 & H)".
       iDestruct "H" as (vl2 vl3) "(% & Ho2 & Ho3)". subst.
@@ -215,7 +215,7 @@ Section typing.
 
   Global Instance prod2_unit_leftid E L : LeftId (eqtype E L) unit product2.
   Proof.
-    intros ty. apply eqtype_unfold. iIntros (?) "_ !# _". iSplit; first done.
+    intros ty. apply eqtype_unfold. iIntros (??) "_ !# _". iSplit; first done.
     iSplit; iIntros "!# *"; iSplit; iIntros "H".
     - iDestruct "H" as (? ?) "(% & % & ?)". by subst.
     - iExists [], _. eauto.
@@ -227,7 +227,7 @@ Section typing.
 
   Global Instance prod2_unit_rightid E L : RightId (eqtype E L) unit product2.
   Proof.
-    intros ty. apply eqtype_unfold. iIntros (?) "_ !# _".
+    intros ty. apply eqtype_unfold. iIntros (??) "_ !# _".
     iSplit; first by rewrite /= -plus_n_O. iSplit; iIntros "!# *"; iSplit; iIntros "H".
     - iDestruct "H" as (? ?) "(% & ? & %)". subst. by rewrite app_nil_r.
     - iExists _, []. rewrite app_nil_r. eauto.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index a28c87860de865c5b8222ba324649142a3468153..3c2ff90b9beffd97008f700926ccb08879251fc2 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -36,12 +36,12 @@ Section product_split.
     (∀ tid ty vl, (ptr ty).(ty_own) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝) →
     ∀ p, tctx_incl E L [p ◁ ptr $ product tyl] (hasty_ptr_offsets p ptr tyl 0).
   Proof.
-    iIntros (Hsplit Hloc p tid q) "#LFT #HE HL H".
+    iIntros (Hsplit Hloc p tid qmax qL) "#LFT #HE HL H".
     iInduction tyl as [|ty tyl IH] "IH" forall (p).
     { rewrite tctx_interp_nil. auto. }
     rewrite product_cons. iMod (Hsplit with "LFT HE HL H") as "(HL & H)".
     cbn -[tctx_elt_interp].
-    iDestruct "H" as "[Hty Htyl]". iDestruct "Hty" as (v) "[Hp Hty]". iDestruct "Hp" as %Hp. 
+    iDestruct "H" as "[Hty Htyl]". iDestruct "Hty" as (v) "[Hp Hty]". iDestruct "Hp" as %Hp.
     iDestruct (Hloc with "Hty") as %[l [=->]].
     iAssert (tctx_elt_interp tid (p +ₗ #0 ◁ ptr ty)) with "[Hty]" as "$".
     { iExists #l. iSplit; last done. simpl; by rewrite Hp shift_loc_0. }
@@ -58,7 +58,7 @@ Section product_split.
     (∀ tid ty vl, (ptr ty).(ty_own) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝) →
     ∀ p, tctx_incl E L (hasty_ptr_offsets p ptr tyl 0) [p ◁ ptr $ product tyl].
   Proof.
-    iIntros (Hptr Htyl Hmerge Hloc p tid q) "#LFT #HE HL H".
+    iIntros (Hptr Htyl Hmerge Hloc p tid qmax qL) "#LFT #HE HL H".
     iInduction tyl as [|ty tyl IH] "IH" forall (p Htyl); first done.
     rewrite product_cons. rewrite /= tctx_interp_singleton tctx_interp_cons.
     iDestruct "H" as "[Hty Htyl]". iDestruct "Hty" as (v) "[Hp Hty]".
@@ -86,7 +86,7 @@ Section product_split.
     tctx_incl E L [p ◁ own_ptr n $ product2 ty1 ty2]
                   [p ◁ own_ptr n ty1; p +ₗ #ty1.(ty_size) ◁ own_ptr n ty2].
   Proof.
-    iIntros (tid q) "#LFT _ $ H".
+    iIntros (tid qmax qL) "#LFT _ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as ([[]|]) "[#Hp H]"; try done.
     iDestruct "H" as "[H >H†]". iDestruct "H" as (vl) "[>H↦ H]".
@@ -104,7 +104,7 @@ Section product_split.
     tctx_incl E L [p ◁ own_ptr n ty1; p +ₗ #ty1.(ty_size) ◁ own_ptr n ty2]
                   [p ◁ own_ptr n $ product2 ty1 ty2].
   Proof.
-    iIntros (tid q) "#LFT _ $ H".
+    iIntros (tid qmax qL) "#LFT _ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "(Hp1 & H1)"; try done.
     iDestruct "H1" as "(H↦1 & H†1)".
@@ -141,7 +141,7 @@ Section product_split.
     tctx_incl E L [p ◁ &uniq{κ}(product2 ty1 ty2)]
                   [p ◁ &uniq{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &uniq{κ} ty2].
   Proof.
-    iIntros (tid q) "#LFT _ $ H".
+    iIntros (tid qmax qL) "#LFT _ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as ([[]|]) "[Hp H]"; try done. iDestruct "Hp" as %Hp.
     rewrite /= split_prod_mt. iMod (bor_sep with "LFT H") as "[H1 H2]"; first solve_ndisj.
@@ -153,7 +153,7 @@ Section product_split.
     tctx_incl E L [p ◁ &uniq{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &uniq{κ} ty2]
                   [p ◁ &uniq{κ}(product2 ty1 ty2)].
   Proof.
-    iIntros (tid q) "#LFT _ $ H".
+    iIntros (tid qmax qL) "#LFT _ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 H1]"; try done.
     iDestruct "Hp1" as %Hp1. iDestruct "H2" as (v2) "(Hp2 & H2)". rewrite /= Hp1.
@@ -190,7 +190,7 @@ Section product_split.
     tctx_incl E L [p ◁ &shr{κ}(product2 ty1 ty2)]
                   [p ◁ &shr{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &shr{κ} ty2].
   Proof.
-    iIntros (tid q) "#LFT _ $ H".
+    iIntros (tid qmax qL) "#LFT _ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as ([[]|]) "[Hp H]"; try iDestruct "H" as "[]".
     iDestruct "H" as "[H1 H2]". iDestruct "Hp" as %Hp.
@@ -201,7 +201,7 @@ Section product_split.
     tctx_incl E L [p ◁ &shr{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &shr{κ} ty2]
                   [p ◁ &shr{κ}(product2 ty1 ty2)].
   Proof.
-    iIntros (tid q) "#LFT _ $ H".
+    iIntros (tid qmax qL) "#LFT _ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 Hown1]"; try done.
     iDestruct "Hp1" as %Hp1. iDestruct "H2" as ([[]|]) "[Hp2 Hown2]"; try done.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 8291216c4453861fbc2dca404113766f4db68fa1..60b717afd00792a78e00276264fd6aaf4cbe154e 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -9,8 +9,8 @@ Section typing.
   (* 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) : iProp Σ :=
-    (∀ tid, lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗ llctx_interp L 1 -∗
-               cctx_interp tid C -∗ tctx_interp tid T -∗
+    (∀ tid (qmax : Qp), lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗ llctx_interp qmax L -∗
+               cctx_interp tid qmax C -∗ tctx_interp tid T -∗
                WP e {{ _, cont_postcondition }})%I.
   Global Arguments typed_body _ _ _ _ _%E.
 
@@ -33,12 +33,22 @@ Section typing.
            (typed_body E L).
   Proof.
     intros C1 C2 HC T1 T2 HT e ? <-. iIntros "H".
-    iIntros (tid) "#LFT #HE Htl HL HC HT".
+    iIntros (tid qmax) "#LFT #HE Htl HL HC HT".
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
     iMod (HT with "LFT HE HL HT") as "(HL & HT)".
+    iDestruct ("HLclose" with "HL") as "HL".
     iApply ("H" with "LFT HE Htl HL [HC] HT").
     by iApply (HC with "LFT HE HC").
   Qed.
 
+  Lemma typed_body_tctx_incl E L T2 T1 C e :
+    tctx_incl E L T1 T2 →
+    (⊢ typed_body E L C T2 e) →
+    ⊢ typed_body E L C T1 e.
+  Proof.
+    intros Hincl He2. iApply typed_body_mono; last done; done.
+  Qed.
+
   Global Instance typed_body_mono_flip E L:
     Proper (cctx_incl E ==> tctx_incl E L ==> eq ==> flip (⊢))
            (typed_body E L).
@@ -47,19 +57,19 @@ Section typing.
   (** Instruction *)
   Definition typed_instruction (E : elctx) (L : llctx)
              (T1 : tctx) (e : expr) (T2 : val → tctx) : iProp Σ :=
-    (∀ tid, lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗
-              llctx_interp L 1 -∗ tctx_interp tid T1 -∗
+    (∀ tid qmax, lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗
+              llctx_interp qmax L -∗ tctx_interp tid T1 -∗
               WP e {{ v, na_own tid ⊤ ∗
-                         llctx_interp L 1 ∗ tctx_interp tid (T2 v) }})%I.
+                         llctx_interp qmax L ∗ tctx_interp tid (T2 v) }})%I.
   Global Arguments typed_instruction _ _ _ _%E _.
 
   (** Writing and Reading **)
   Definition typed_write_def (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
-    (□ ∀ v tid F qL, ⌜lftE ∪ (↑lrustN) ⊆ F⌝ →
-      lft_ctx -∗ elctx_interp E -∗ llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
+    (□ ∀ v tid F qmax qL, ⌜lftE ∪ (↑lrustN) ⊆ F⌝ →
+      lft_ctx -∗ elctx_interp E -∗ llctx_interp_noend qmax L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
         ∃ (l : loc) vl, ⌜length vl = ty.(ty_size) ∧ v = #l⌝ ∗ l ↦∗ vl ∗
           (▷ l ↦∗: ty.(ty_own) tid ={F}=∗
-            llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
+            llctx_interp_noend qmax L qL ∗ ty2.(ty_own) tid [v]))%I.
   Definition typed_write_aux : seal (@typed_write_def). by eexists. Qed.
   Definition typed_write := typed_write_aux.(unseal).
   Definition typed_write_eq : @typed_write = @typed_write_def := typed_write_aux.(seal_eq).
@@ -75,12 +85,12 @@ Section typing.
      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_def (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
-    (□ ∀ v tid F qL, ⌜lftE ∪ ↑lrustN ⊆ F⌝ →
+    (□ ∀ v tid F qmax qL, ⌜lftE ∪ ↑lrustN ⊆ F⌝ →
       lft_ctx -∗ elctx_interp E -∗ na_own tid F -∗
-      llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
+      llctx_interp_noend qmax L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
         ∃ (l : loc) vl q, ⌜v = #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.
+                              llctx_interp_noend qmax L qL ∗ ty2.(ty_own) tid [v]))%I.
   Definition typed_read_aux : seal (@typed_read_def). by eexists. Qed.
   Definition typed_read := typed_read_aux.(unseal).
   Definition typed_read_eq : @typed_read = @typed_read_def := typed_read_aux.(seal_eq).
@@ -109,25 +119,27 @@ Section typing_rules.
     typed_body E L C T e -∗ typed_body E L C T e.
   Proof. done. Qed.
 
-  (* TODO: Proof a version of this that substitutes into a compatible context...
-     if we really want to do that. *)
-  Lemma type_equivalize_lft E L C T κ1 κ2 e :
-    (⊢ typed_body ((κ1 ⊑ₑ κ2) :: (κ2 ⊑ₑ κ1) :: E) L C T e) →
-    ⊢ typed_body E ((κ1 ⊑ₗ [κ2]) :: L) C T e.
+  (** This version is *weaker* than what was in the original paper;
+  it had to be adjusted for GhostCell. *)
+  Lemma type_equivalize_lft E L C T1 T2 κ1 κ2 e :
+    (∀ tid, lft_ctx -∗ κ1 ⊑ κ2 -∗ κ2 ⊑ κ1 -∗ tctx_interp tid T1 -∗ tctx_interp tid T2) →
+    (⊢ typed_body E L C T2 e) →
+    ⊢ typed_body E ((κ1 ⊑ₗ [κ2]) :: L) C T1 e.
   Proof.
-    iIntros (He tid) "#LFT #HE Htl [Hκ HL] HC HT".
-    iMod (lctx_equalize_lft with "LFT Hκ") as "[Hκ1 Hκ2]".
-    iApply (He with "LFT [Hκ1 Hκ2 HE] Htl HL HC HT").
-    rewrite /elctx_interp /=. by iFrame.
+    iIntros (Hswitch He tid qmax) "#LFT #HE Htl [Hκ HL] HC HT".
+    iMod (lctx_equalize_lft_sem with "LFT Hκ") as "[Hκ1 Hκ2]".
+    iApply (He with "LFT HE Htl HL HC [-]").
+    iApply (Hswitch with "LFT Hκ1 Hκ2"). done.
   Qed.
-  Lemma type_equivalize_lft_static E L C T κ e :
-    (⊢ typed_body ((static ⊑ₑ κ) :: E) L C T e) →
-    ⊢ typed_body E ((κ ⊑ₗ []) :: L) C T e.
+  Lemma type_equivalize_lft_static E L C T1 T2 κ e :
+    (∀ tid, lft_ctx -∗ static ⊑ κ -∗ tctx_interp tid T1 -∗ tctx_interp tid T2) →
+    (⊢ typed_body E L C T2 e) →
+    ⊢ typed_body E ((κ ⊑ₗ []) :: L) C T1 e.
   Proof.
-    iIntros (He tid) "#LFT #HE Htl [Hκ HL] HC HT".
-    iMod (lctx_equalize_lft_static with "LFT Hκ") as "Hκ_static".
-    iApply (He with "LFT [Hκ_static HE] Htl HL HC HT").
-    rewrite /elctx_interp /=. by iFrame.
+    iIntros (Hswitch He tid qmax) "#LFT #HE Htl [Hκ HL] HC HT".
+    iMod (lctx_equalize_lft_sem_static with "LFT Hκ") as "Hκ".
+    iApply (He with "LFT HE Htl HL HC [-]").
+    iApply (Hswitch with "LFT Hκ"). done.
   Qed.
 
   Lemma type_let' E L T1 T2 (T : tctx) C xb e e' :
@@ -136,7 +148,7 @@ Section typing_rules.
     (∀ v : val, typed_body E L C (T2 v ++ T) (subst' xb v e')) -∗
     typed_body E L C (T1 ++ T) (let: xb := e in e').
   Proof.
-    iIntros (Hc) "He He'". iIntros (tid) "#LFT #HE Htl HL HC HT". rewrite tctx_interp_app.
+    iIntros (Hc) "He He'". iIntros (tid qmax) "#LFT #HE Htl HL HC HT". rewrite tctx_interp_app.
     iDestruct "HT" as "[HT1 HT]". wp_bind e. iApply (wp_wand with "[He HL HT1 Htl]").
     { iApply ("He" with "LFT HE Htl HL HT1"). }
     iIntros (v) "/= (Htl & HL & HT2)". wp_let.
@@ -173,12 +185,16 @@ Section typing_rules.
     (∀ κ, typed_body E ((κ ⊑ₗ κs) :: L) C T e) -∗
     typed_body E L C T (Newlft ;; e).
   Proof.
-    iIntros (Hc) "He". iIntros (tid) "#LFT #HE Htl HL HC HT".
+    iIntros (Hc) "He". iIntros (tid qmax) "#LFT #HE Htl HL HC HT".
     iMod (lft_create with "LFT") as (Λ) "[Htk #Hinh]"; first done.
     set (κ' := lft_intersect_list κs). wp_seq.
     iApply ("He" $! (κ' ⊓ Λ) with "LFT HE Htl [HL Htk] HC HT").
     rewrite /llctx_interp /=. iFrame "HL".
-    iExists Λ. iSplit; first done. iFrame. done.
+    iExists Λ. iSplit; first done.
+    destruct (decide (1 ≤ qmax)%Qp) as [_|Hlt%Qp_lt_nge].
+    - by iFrame "#∗".
+    - apply Qp_lt_sum in Hlt as [q' ->]. iDestruct "Htk" as "[$ Htk]".
+      iIntros "Htk'". iApply "Hinh". iFrame.
   Qed.
 
   (* TODO: It should be possible to show this while taking only one step.
@@ -187,8 +203,8 @@ Section typing_rules.
     Closed [] e → UnblockTctx κ T1 T2 →
     typed_body E L C T2 e -∗ typed_body E ((κ ⊑ₗ κs) :: L) C T1 (Endlft ;; e).
   Proof.
-    iIntros (Hc Hub) "He". iIntros (tid) "#LFT #HE Htl [Hκ HL] HC HT".
-    iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
+    iIntros (Hc Hub) "He". iIntros (tid qmax) "#LFT #HE Htl [Hκ HL] HC HT".
+    iDestruct "Hκ" as (Λ) "(% & Htok & Hend)".
     iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
     iApply (wp_mask_mono _ (↑lftN ∪ ↑lft_userN)); first done.
     iApply (wp_step_fupd with "Hend"); first set_solver-. wp_seq.
@@ -199,7 +215,7 @@ Section typing_rules.
   Lemma type_path_instr {E L} p ty :
     ⊢ typed_instruction_ty E L [p ◁ ty] p ty.
   Proof.
-    iIntros (?) "_ _ $$ [? _]".
+    iIntros (??) "_ _ $$ [? _]".
     iApply (wp_hasty with "[-]"). done. iIntros (v) "_ Hv".
     rewrite tctx_interp_singleton. iExists v. iFrame. by rewrite eval_path_of_val.
   Qed.
@@ -215,18 +231,20 @@ Section typing_rules.
     (⊢ typed_write E L ty1 ty ty1') →
     (⊢ typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <- p2) (λ _, [p1 ◁ ty1'])).
   Proof.
-    iIntros (Hwrt tid) "#LFT #HE $ HL".
+    iIntros (Hwrt tid ?) "#LFT #HE $ HL".
     rewrite tctx_interp_cons tctx_interp_singleton. iIntros "[Hp1 Hp2]".
     wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
     wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "_ Hown2".
     rewrite typed_write_eq in Hwrt.
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
     iMod (Hwrt with "[] LFT HE HL Hown1") as (l vl) "([% %] & Hl & Hclose)"; first done.
     subst v1. iDestruct (ty_size_eq with "Hown2") as "#Hsz". iDestruct "Hsz" as %Hsz.
     rewrite <-Hsz in *. destruct vl as [|v[|]]; try done.
     rewrite heap_mapsto_vec_singleton. iApply wp_fupd. wp_write.
     rewrite -heap_mapsto_vec_singleton.
-    iMod ("Hclose" with "[Hl Hown2]") as "($ & Hown)".
+    iMod ("Hclose" with "[Hl Hown2]") as "(HL & Hown)".
     { iExists _. iFrame. }
+    iDestruct ("HLclose" with "HL") as "$".
     rewrite tctx_interp_singleton tctx_hasty_val' //.
   Qed.
 
@@ -242,16 +260,18 @@ Section typing_rules.
     ty.(ty_size) = 1%nat → (⊢ typed_read E L ty1 ty ty1') →
     (⊢ typed_instruction E L [p ◁ ty1] (!p) (λ v, [p ◁ ty1'; v ◁ ty])).
   Proof.
-    iIntros (Hsz Hread tid) "#LFT #HE Htl HL Hp".
+    iIntros (Hsz Hread tid qmax) "#LFT #HE Htl HL Hp".
     rewrite tctx_interp_singleton. wp_bind p. iApply (wp_hasty with "Hp").
     iIntros (v) "% Hown".
     rewrite typed_read_eq in Hread.
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
     iMod (Hread with "[] LFT HE Htl HL Hown") as
         (l vl q) "(% & Hl & Hown & Hclose)"; first done.
     subst v. iDestruct (ty_size_eq with "Hown") as "#>%". rewrite ->Hsz in *.
     destruct vl as [|v [|]]; try done.
     rewrite heap_mapsto_vec_singleton. iApply wp_fupd. wp_read.
-    iMod ("Hclose" with "Hl") as "($ & $ & Hown2)".
+    iMod ("Hclose" with "Hl") as "($ & HL & Hown2)".
+    iDestruct ("HLclose" with "HL") as "$".
     rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
     by iFrame.
   Qed.
@@ -265,13 +285,13 @@ Section typing_rules.
     typed_body E L C T (let: x := !p in e).
   Proof. iIntros. by iApply type_let; [apply type_deref_instr|solve_typing|]. Qed.
 
-  Lemma type_memcpy_iris E L qL tid ty ty1 ty1' ty2 ty2' (n : Z) p1 p2 :
+  Lemma type_memcpy_iris E L qmax 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 ∗
+    {{{ lft_ctx ∗ elctx_interp E ∗ na_own tid ⊤ ∗ llctx_interp_noend qmax 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 ∗
+    {{{ RET #☠; na_own tid ⊤ ∗ llctx_interp_noend qmax L qL ∗
                  tctx_elt_interp tid (p1 ◁ ty1') ∗ tctx_elt_interp tid (p2 ◁ ty2') }}}.
   Proof.
     iIntros (<-) "#Hwrt #Hread !#".
@@ -298,10 +318,12 @@ Section typing_rules.
     ⊢ typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2] (p1 <-{n} !p2)
                       (λ _, [p1 ◁ ty1'; p2 ◁ ty2']).
   Proof.
-    iIntros (Hsz Hwrt Hread tid) "#LFT #HE Htl HL HT".
+    iIntros (Hsz Hwrt Hread tid qmax) "#LFT #HE Htl HL HT".
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
     iApply (type_memcpy_iris with "[] [] [$LFT $Htl $HE $HL HT]"); try done.
     { by rewrite tctx_interp_cons tctx_interp_singleton. }
-    rewrite tctx_interp_cons tctx_interp_singleton. auto.
+    rewrite tctx_interp_cons tctx_interp_singleton.
+    iIntros "!> ($ & HL & $ & $)". by iApply "HLclose".
   Qed.
 
   Lemma type_memcpy {E L} ty ty1 ty2 (n : Z) C T T' ty1' ty2' p1 p2 e:
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 99690914f786a7ae128999bdddffbac90bb6b349..18b0c8176040df21fbcd04248a3bbae97267530b 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -30,10 +30,11 @@ Section shr_bor.
     Proper (flip (lctx_lft_incl E L) ==> subtype E L ==> subtype E L) shr_bor.
   Proof.
     intros κ1 κ2 Hκ ty1 ty2 Hty.
-    iIntros (?) "/= HL". iDestruct (Hκ with "HL") as "#Hincl".
+    iIntros (??) "/= HL". iDestruct (Hκ with "HL") as "#Hincl".
     iDestruct (Hty with "HL") as "#Hty". iIntros "!# #HE".
+    iDestruct ("Hincl" with "HE") as "%".
     iApply shr_type_incl.
-    - by iApply "Hincl".
+    - by iApply lft_incl_syn_sem.
     - by iApply "Hty".
   Qed.
   Global Instance shr_mono_flip E L :
@@ -74,10 +75,11 @@ Section typing.
     lctx_lft_incl E L κ' κ →
     tctx_incl E L [p ◁ &shr{κ}ty] [p ◁ &shr{κ'}ty; p ◁{κ} &shr{κ}ty].
   Proof.
-    iIntros (Hκκ' tid ?) "#LFT #HE HL [H _]". iDestruct (Hκκ' with "HL HE") as "#Hκκ'".
+    iIntros (Hκκ' tid ??) "#LFT #HE HL [H _]". iDestruct (Hκκ' with "HL HE") as "%".
     iFrame. rewrite /tctx_interp /=.
     iDestruct "H" as ([[]|]) "[% #Hshr]"; try done. iModIntro. iSplit.
-    - iExists _. iSplit. done. by iApply (ty_shr_mono with "Hκκ' Hshr").
+    - iExists _. iSplit. done. iApply (ty_shr_mono with "[] Hshr").
+      by iApply lft_incl_syn_sem.
     - iSplit=> //. iExists _. auto.
   Qed.
 
@@ -85,7 +87,7 @@ Section typing.
     Copy ty → lctx_lft_alive E L κ → ⊢ typed_read E L (&shr{κ}ty) ty (&shr{κ}ty).
   Proof.
     rewrite typed_read_eq. iIntros (Hcopy Halive) "!#".
-    iIntros ([[]|] tid F qL ?) "#LFT #HE Htl HL #Hshr"; try done.
+    iIntros ([[]|] tid F qmax qL ?) "#LFT #HE Htl HL #Hshr"; try done.
     iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first solve_ndisj.
     iMod (copy_shr_acc with "LFT Hshr Htl Hκ") as (q') "(Htl & H↦ & Hcl)"; first solve_ndisj.
     { rewrite ->shr_locsE_shrN. solve_ndisj. }
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 6157b9a8542db5cd9e35df64332ecdf384bb6439..7f3fa099052046c9bab4d45997701c507872b51b 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -38,7 +38,7 @@ Section type_soundness.
     iMod lft_init as (?) "#LFT". done.
     iMod na_alloc as (tid) "Htl". set (Htype := TypeG _ _ _ _ _).
     wp_bind (of_val main). iApply (wp_wand with "[Htl]").
-    iApply (Hmain Htype [] [] $! tid with "LFT [] Htl [] []").
+    iApply (Hmain Htype [] [] $! tid 1%Qp with "LFT [] Htl [] []").
     { by rewrite /elctx_interp big_sepL_nil. }
     { by rewrite /llctx_interp big_sepL_nil. }
     { by rewrite tctx_interp_nil. }
@@ -48,10 +48,13 @@ Section type_soundness.
     iDestruct "Hmain" as (f k x e ?) "(EQ & % & Hmain)". iDestruct "EQ" as %[= ->].
     destruct x; try done. wp_rec.
     iMod (lft_create with "LFT") as (ϝ) "Hϝ"; first done.
-    iApply ("Hmain" $! () ϝ exit_cont [#] tid with "LFT [] Htl [Hϝ] []");
+    iApply ("Hmain" $! () ϝ exit_cont [#] tid 1%Qp with "LFT [] Htl [Hϝ] []");
       last by rewrite tctx_interp_nil.
     { by rewrite /elctx_interp /=. }
-    { rewrite /llctx_interp /=. iSplit; last done. iExists ϝ. iFrame. by rewrite /= left_id. }
+    { rewrite /llctx_interp /=. iSplit; last done. iExists ϝ.
+      rewrite /= left_id. iSplit; first done.
+      rewrite decide_True //.
+      by iDestruct "Hϝ" as "[$ #$]". }
     rewrite cctx_interp_singleton. simpl. iIntros (args) "_ _".
     inv_vec args. iIntros (x) "_ /=". by wp_lam.
   Qed.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 2d8c32adc4c349465762cace5e04820d976c345c..55e1a493cc528db93a167ae4e2fe4cf5b4983ba0 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -125,14 +125,14 @@ Section sum.
   Global Instance sum_mono E L :
     Proper (Forall2 (subtype E L) ==> subtype E L) sum.
   Proof.
-    iIntros (tyl1 tyl2 Htyl qL) "HL".
+    iIntros (tyl1 tyl2 Htyl qmax qL) "HL".
     iAssert (□ (lft_contexts.elctx_interp E -∗ ⌜max_list_with ty_size tyl1 = max_list_with ty_size tyl2⌝))%I with "[#]" as "#Hleq".
     { iInduction Htyl as [|???? Hsub] "IH".
       { iClear "∗". iIntros "!# _". done. }
       iDestruct (Hsub with "HL") as "#Hsub". iDestruct ("IH" with "HL") as "{IH} #IH".
       iModIntro. iIntros "#HE". iDestruct ("Hsub" with "HE") as "(% & _ & _)".
       iDestruct ("IH" with "HE") as %IH. iPureIntro. simpl. inversion_clear IH. by f_equal. }
-    iDestruct (subtype_Forall2_llctx with "HL") as "#Htyl"; first done.
+    iDestruct (subtype_Forall2_llctx_noend with "HL") as "#Htyl"; first done.
     iClear "HL". iIntros "!# #HE".
     iDestruct ("Hleq" with "HE") as %Hleq. iSpecialize ("Htyl" with "HE"). iClear "Hleq HE".
     iAssert (∀ i, type_incl (nth i tyl1 emp0) (nth i tyl2 emp0))%I with "[#]" as "#Hty".
diff --git a/theories/typing/type.v b/theories/typing/type.v
index dcbd4c113db2e276a068d616e5bcd90414956300..6cfae95147b63fab03b09efa129a7d57872d409c 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -540,8 +540,14 @@ Definition type_incl `{!typeG Σ} (ty1 ty2 : type) : iProp Σ :=
 Instance: Params (@type_incl) 2 := {}.
 (* Typeclasses Opaque type_incl. *)
 
+Definition type_equal `{!typeG Σ} (ty1 ty2 : type) : iProp Σ :=
+    (⌜ty1.(ty_size) = ty2.(ty_size)⌝ ∗
+     (□ ∀ tid vl, ty1.(ty_own) tid vl ∗-∗ ty2.(ty_own) tid vl) ∗
+     (□ ∀ κ tid l, ty1.(ty_shr) κ tid l ∗-∗ ty2.(ty_shr) κ tid l))%I.
+Instance: Params (@type_equal) 2 := {}.
+
 Definition subtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
-  ∀ qL, llctx_interp L qL -∗ □ (elctx_interp E -∗ type_incl ty1 ty2).
+  ∀ qmax qL, llctx_interp_noend qmax L qL -∗ □ (elctx_interp E -∗ type_incl ty1 ty2).
 Instance: Params (@subtype) 4 := {}.
 
 (* TODO: The prelude should have a symmetric closure. *)
@@ -574,20 +580,20 @@ Section subtyping.
   Qed.
 
   Lemma subtype_refl E L ty : subtype E L ty ty.
-  Proof. iIntros (?) "_ !# _". iApply type_incl_refl. Qed.
+  Proof. iIntros (??) "_ !# _". iApply type_incl_refl. Qed.
   Global Instance subtype_preorder E L : PreOrder (subtype E L).
   Proof.
     split; first by intros ?; apply subtype_refl.
-    intros ty1 ty2 ty3 H12 H23. iIntros (?) "HL".
+    iIntros (ty1 ty2 ty3 H12 H23 ??) "HL".
     iDestruct (H12 with "HL") as "#H12".
     iDestruct (H23 with "HL") as "#H23".
     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_noend E L tys1 tys2 qmax qL :
     Forall2 (subtype E L) tys1 tys2 →
-    llctx_interp L qL -∗ □ (elctx_interp E -∗
+    llctx_interp_noend qmax L qL -∗ □ (elctx_interp E -∗
            [∗ list] tys ∈ (zip tys1 tys2), type_incl (tys.1) (tys.2)).
   Proof.
     iIntros (Htys) "HL".
@@ -600,18 +606,53 @@ Section subtyping.
     iIntros "!# * % #Hincl". by iApply "Hincl".
   Qed.
 
+  Lemma subtype_Forall2_llctx E L tys1 tys2 qmax :
+    Forall2 (subtype E L) tys1 tys2 →
+    llctx_interp qmax L -∗ □ (elctx_interp E -∗
+           [∗ list] tys ∈ (zip tys1 tys2), type_incl (tys.1) (tys.2)).
+  Proof.
+    iIntros (?) "HL". iApply subtype_Forall2_llctx_noend; first done.
+    iDestruct (llctx_interp_acc_noend with "HL") as "[$ _]".
+  Qed.
+
+  Lemma type_equal_incl ty1 ty2 :
+    type_equal ty1 ty2 ⊣⊢ type_incl ty1 ty2 ∗ type_incl ty2 ty1.
+  Proof.
+    iSplit.
+    - iIntros "#(% & Ho & Hs)".
+      iSplit; (iSplit; first done; iSplit; iModIntro).
+      + iIntros (??) "?". by iApply "Ho".
+      + iIntros (???) "?". by iApply "Hs".
+      + iIntros (??) "?". by iApply "Ho".
+      + iIntros (???) "?". by iApply "Hs".
+    - iIntros "#[(% & Ho1 & Hs1) (% & Ho2 & Hs2)]".
+      iSplit; first done. iSplit; iModIntro.
+      + iIntros (??). iSplit; [iApply "Ho1"|iApply "Ho2"].
+      + iIntros (???). iSplit; [iApply "Hs1"|iApply "Hs2"].
+  Qed.
+
+  Lemma type_equal_refl ty :
+    ⊢ type_equal ty ty.
+  Proof.
+    iApply type_equal_incl. iSplit; iApply type_incl_refl.
+  Qed.
+  Lemma type_equal_trans ty1 ty2 ty3 :
+    type_equal ty1 ty2 -∗ type_equal ty2 ty3 -∗ type_equal ty1 ty3.
+  Proof.
+    rewrite !type_equal_incl. iIntros "#[??] #[??]". iSplit.
+    - iApply (type_incl_trans _ ty2); done.
+    - iApply (type_incl_trans _ ty2); done.
+  Qed.
+
   Lemma equiv_subtype E L ty1 ty2 : ty1 ≡ ty2 → subtype E L ty1 ty2.
   Proof. unfold subtype, type_incl=>EQ. setoid_rewrite EQ. apply subtype_refl. Qed.
 
   Lemma eqtype_unfold E L ty1 ty2 :
     eqtype E L ty1 ty2 ↔
-    (∀ qL, llctx_interp L qL -∗ □ (elctx_interp E -∗
-      (⌜ty1.(ty_size) = ty2.(ty_size)⌝ ∗
-      (□ ∀ tid vl, ty1.(ty_own) tid vl ↔ ty2.(ty_own) tid vl) ∗
-      (□ ∀ κ tid l, ty1.(ty_shr) κ tid l ↔ ty2.(ty_shr) κ tid l)))%I).
+    (∀ qmax qL, llctx_interp_noend qmax L qL -∗ □ (elctx_interp E -∗ type_equal ty1 ty2)).
   Proof.
     split.
-    - iIntros ([EQ1 EQ2] qL) "HL".
+    - iIntros ([EQ1 EQ2] qmax qL) "HL".
       iDestruct (EQ1 with "HL") as "#EQ1".
       iDestruct (EQ2 with "HL") as "#EQ2".
       iClear "∗". iIntros "!# #HE".
@@ -621,7 +662,7 @@ Section subtyping.
       + done.
       + by iIntros "!#*"; iSplit; iIntros "H"; [iApply "H1own"|iApply "H2own"].
       + by iIntros "!#*"; iSplit; iIntros "H"; [iApply "H1shr"|iApply "H2shr"].
-    - intros EQ. split; (iIntros (qL) "HL";
+    - intros EQ. split; (iIntros (qmax qL) "HL";
       iDestruct (EQ with "HL") as "#EQ";
       iClear "∗"; iIntros "!# #HE";
       iDestruct ("EQ" with "HE") as "[% [#Hown #Hshr]]";
@@ -663,11 +704,11 @@ Section subtyping.
   Qed.
 
   Lemma subtype_simple_type E L (st1 st2 : simple_type) :
-    (∀ qL, llctx_interp L qL -∗ □ (elctx_interp E -∗
+    (∀ qmax qL, llctx_interp_noend qmax L qL -∗ □ (elctx_interp E -∗
        ∀ tid vl, st1.(st_own) tid vl -∗ st2.(st_own) tid vl)) →
     subtype E L st1 st2.
   Proof.
-    intros Hst. iIntros (qL) "HL". iDestruct (Hst with "HL") as "#Hst".
+    intros Hst. iIntros (qmax qL) "HL". iDestruct (Hst with "HL") as "#Hst".
     iClear "∗". iIntros "!# #HE". iApply type_incl_simple_type.
     iIntros "!#" (??) "?". by iApply "Hst".
   Qed.
@@ -676,7 +717,7 @@ Section subtyping.
     E1 ⊆+ E2 → L1 ⊆+ L2 →
     subtype E1 L1 ty1 ty2 → subtype E2 L2 ty1 ty2.
   Proof.
-    iIntros (HE12 ? Hsub qL) "HL". iDestruct (Hsub with "[HL]") as "#Hsub".
+    iIntros (HE12 ? Hsub qmax qL) "HL". iDestruct (Hsub with "[HL]") as "#Hsub".
     { rewrite /llctx_interp. by iApply big_sepL_submseteq. }
     iClear "∗". iIntros "!# #HE". iApply "Hsub".
     rewrite /elctx_interp. by iApply big_sepL_submseteq.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index b73bd978fe85cc8105014d5b966edf684968b0fd..ce685e63d5fc967fc70674309db5b0d980aeb839 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -164,28 +164,28 @@ Section type_context.
 
   (** Type context inclusion *)
   Definition tctx_incl (E : elctx) (L : llctx) (T1 T2 : tctx): Prop :=
-    ∀ tid q2, lft_ctx -∗ elctx_interp E -∗ llctx_interp L q2 -∗
-              tctx_interp tid T1 ={⊤}=∗ llctx_interp L q2 ∗ tctx_interp tid T2.
+    ∀ tid qmax q2, lft_ctx -∗ elctx_interp E -∗ llctx_interp_noend qmax L q2 -∗
+              tctx_interp tid T1 ={⊤}=∗ llctx_interp_noend qmax L q2 ∗ tctx_interp tid T2.
   Global Instance : ∀ E L, RewriteRelation (tctx_incl E L) := {}.
 
   Global Instance tctx_incl_preorder E L : PreOrder (tctx_incl E L).
   Proof.
     split.
-    - by iIntros (???) "_ _ $ $".
-    - iIntros (??? H1 H2 ??) "#LFT #HE HL H".
+    - by iIntros (????) "_ _ $ $".
+    - iIntros (??? H1 H2 ???) "#LFT #HE HL H".
       iMod (H1 with "LFT HE HL H") as "(HL & H)".
       by iMod (H2 with "LFT HE HL H") as "($ & $)".
   Qed.
 
   Lemma contains_tctx_incl E L T1 T2 : T1 ⊆+ T2 → tctx_incl E L T2 T1.
   Proof.
-    rewrite /tctx_incl. iIntros (Hc ??) "_ _ $ H". by iApply big_sepL_submseteq.
+    rewrite /tctx_incl. iIntros (Hc ???) "_ _ $ H". by iApply big_sepL_submseteq.
   Qed.
 
   Global Instance tctx_incl_app E L :
     Proper (tctx_incl E L ==> tctx_incl E L ==> tctx_incl E L) app.
   Proof.
-    intros ?? Hincl1 ?? Hincl2 ??. rewrite /tctx_interp !big_sepL_app.
+    intros ?? Hincl1 ?? Hincl2 ???. rewrite /tctx_interp !big_sepL_app.
     iIntros "#LFT #HE HL [H1 H2]".
     iMod (Hincl1 with "LFT HE HL H1") as "(HL & $)".
     iApply (Hincl2 with "LFT HE HL H2").
@@ -203,7 +203,7 @@ Section type_context.
 
   Lemma copy_tctx_incl E L p `{!Copy ty} :
     tctx_incl E L [p ◁ ty] [p ◁ ty; p ◁ ty].
-  Proof. iIntros (??) "_ _ $ * [#$ $] //". Qed.
+  Proof. iIntros (???) "_ _ $ * [#$ $] //". Qed.
 
   Lemma copy_elem_of_tctx_incl E L T p `{!Copy ty} :
     p ◁ ty ∈ T → tctx_incl E L T ((p ◁ ty) :: T).
@@ -214,12 +214,20 @@ Section type_context.
       apply contains_tctx_incl, submseteq_swap.
   Qed.
 
+  Lemma type_incl_tctx_incl tid p ty1 ty2 :
+    type_incl ty1 ty2 -∗ tctx_interp tid [p ◁ ty1] -∗ tctx_interp tid [p ◁ ty2].
+  Proof.
+    iIntros "Hincl HT". rewrite !tctx_interp_singleton.
+    iDestruct "HT" as (v) "[% HT]". iExists _. iFrame "%".
+    iDestruct "Hincl" as "(_ & Hincl & _)". iApply "Hincl". done.
+  Qed.
   Lemma subtype_tctx_incl E L p ty1 ty2 :
     subtype E L ty1 ty2 → tctx_incl E L [p ◁ ty1] [p ◁ ty2].
   Proof.
-    iIntros (Hst ??) "#LFT #HE HL [H _]".
-    iDestruct "H" as (v) "[% H]". iDestruct (Hst with "HL HE") as "#(_ & Ho & _)". 
-    iFrame "HL". iApply big_sepL_singleton. iExists _. iFrame "%". by iApply "Ho".
+    iIntros (Hst ???) "#LFT #HE HL HT".
+    iDestruct (Hst with "HL") as "#Hst". iFrame "HL".
+    iApply type_incl_tctx_incl; last done.
+    by iApply "Hst".
   Qed.
 
   (* Extracting from a type context. *)
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index a8c4d60bf69d88afe64915395f00dbb15b5107dc..b0a513f9b86dd412ea806c5969f3ebae2e8c215b 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -17,7 +17,7 @@ Section case.
       tyl el →
     ⊢ typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T) (case: !p of el).
   Proof.
-    iIntros (Hel tid) "#LFT #HE Hna HL HC HT". wp_bind p.
+    iIntros (Hel tid qmax) "#LFT #HE Hna HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
     iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try done.
     iDestruct "Hp" as "[H↦ Hf]". iDestruct "H↦" as (vl) "[H↦ Hown]".
@@ -63,9 +63,10 @@ Section case.
       (⊢ typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T) e)) tyl el →
     ⊢ typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T) (case: !p of el).
   Proof.
-    iIntros (Halive Hel tid) "#LFT #HE Hna HL HC HT". wp_bind p.
+    iIntros (Halive Hel tid qmax) "#LFT #HE Hna HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
     iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try iDestruct "Hp" as "[]".
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
     iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
     iMod (bor_acc_cons with "LFT Hp Htok") as "[H↦ Hclose']". done.
     iDestruct "H↦" as (vl) "[H↦ Hown]".
@@ -88,6 +89,7 @@ Section case.
         rewrite /= -EQlen !app_length EQlenvl' EQlenvl'2 nth_lookup EQty /=. auto. }
       { iExists vl'. iFrame. }
       iMod ("Hclose" with "Htok") as "HL".
+      iDestruct ("HLclose" with "HL") as "HL".
       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]";
@@ -96,6 +98,7 @@ Section case.
         rewrite heap_mapsto_vec_cons heap_mapsto_vec_app /= -EQlen. iFrame. iNext.
         iExists i, vl', vl''. rewrite nth_lookup EQty. auto. }
       iMod ("Hclose" with "Htok") as "HL".
+      iDestruct ("HLclose" with "HL") as "HL".
       iApply (Hety with "LFT HE Hna HL HC").
       rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame.
   Qed.
@@ -116,10 +119,11 @@ Section case.
       (⊢ typed_body E L C ((p ◁ &shr{κ}(sum tyl)) :: T) e)) tyl el →
     ⊢ typed_body E L C ((p ◁ &shr{κ}(sum tyl)) :: T) (case: !p of el).
   Proof.
-    iIntros (Halive Hel tid) "#LFT #HE Hna HL HC HT". wp_bind p.
+    iIntros (Halive Hel tid qmax) "#LFT #HE Hna HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
     iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try done.
     iDestruct "Hp" as (i) "[#Hb Hshr]".
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
     iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
     iMod (frac_bor_acc with "LFT Hb Htok") as (q') "[[H↦i H↦vl''] Hclose']". done.
     rewrite nth_lookup.
@@ -128,6 +132,7 @@ Section case.
     wp_read. wp_case; first (split; [lia|by rewrite Nat2Z.id]).
     iMod ("Hclose'" with "[$H↦i $H↦vl'']") as "Htok".
     iMod ("Hclose" with "Htok") as "HL".
+    iDestruct ("HLclose" with "HL") 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. auto.
@@ -148,12 +153,13 @@ Section case.
     (⊢ typed_write E L ty1 (sum tyl) ty2) →
     ⊢ typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <-{Σ i} p2) (λ _, [p1 ◁ ty2]).
   Proof.
-    iIntros (Hty Hw tid) "#LFT #HE $ HL Hp".
+    iIntros (Hty Hw tid qmax) "#LFT #HE $ HL Hp".
     rewrite tctx_interp_cons tctx_interp_singleton.
     iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
     iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
     iApply (wp_hasty with "Hp1"). iIntros (v1 Hv1) "Hty1".
     rewrite typed_write_eq in Hw.
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
     iMod (Hw with "[] LFT HE HL Hty1") as (l vl) "(H & H↦ & Hw)"=>//=.
     destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
     rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
@@ -165,7 +171,10 @@ Section case.
       - intros [= ->]. simpl in *. lia.
       - apply IHtyl. simpl in *. lia. }
     rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦vl" as "[H↦ H↦vl]". wp_write.
-    rewrite tctx_interp_singleton tctx_hasty_val' //. iApply "Hw". iNext.
+    rewrite tctx_interp_singleton tctx_hasty_val' //.
+    iMod ("Hw" with "[-HLclose]") as "[HL $]"; last first.
+    { iApply "HLclose". done. }
+    iNext.
     iExists (_::_::_). rewrite !heap_mapsto_vec_cons. iFrame.
     iExists i, [_], _. rewrite -Hlen nth_lookup Hty. auto.
   Qed.
@@ -189,14 +198,17 @@ Section case.
     (⊢ typed_write E L ty1 (sum tyl) ty2) →
     ⊢ typed_instruction E L [p ◁ ty1] (p <-{Σ i} ()) (λ _, [p ◁ ty2]).
   Proof.
-    iIntros (Hty Hw tid) "#LFT #HE $ HL Hp". rewrite tctx_interp_singleton.
+    iIntros (Hty Hw tid qmax) "#LFT #HE $ HL Hp". rewrite tctx_interp_singleton.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hty".
     rewrite typed_write_eq in Hw.
-    iMod (Hw with "[] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)"; first done.
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
+    iMod (Hw with "[] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". done.
     simpl. destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
     rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl]".
     wp_write. rewrite tctx_interp_singleton tctx_hasty_val' //.
-    iApply "Hw". iModIntro. iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame.
+    iMod ("Hw" with "[-HLclose]") as "[HL $]"; last first.
+    { iApply "HLclose". done. }
+    iModIntro. iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame.
     iExists i, [], _. rewrite -Hlen nth_lookup Hty. auto.
   Qed.
 
@@ -221,7 +233,8 @@ Section case.
     ⊢ typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2]
                (p1 <-{ty.(ty_size),Σ i} !p2) (λ _, [p1 ◁ ty1'; p2 ◁ ty2']).
   Proof.
-    iIntros (Hty Hw Hr tid) "#LFT #HE Htl [HL1 HL2] Hp".
+    iIntros (Hty Hw Hr tid qmax) "#LFT #HE Htl HL Hp".
+    iDestruct (llctx_interp_acc_noend with "HL") as "[[HL1 HL2] HLclose]".
     rewrite tctx_interp_cons tctx_interp_singleton.
     iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
     iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
@@ -245,7 +258,10 @@ Section case.
     { rewrite take_length. lia. }
     iNext; iIntros "[H↦vl1 H↦2]".
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //.
-    iMod ("Hr" with "H↦2") as "($ & $ & $)". iApply "Hw". iNext.
+    iMod ("Hr" with "H↦2") as "($ & HL1 & $)".
+    iMod ("Hw" with "[-HLclose HL1]") as "[HL $]"; last first.
+    { iApply "HLclose". by iFrame. }
+    iNext.
     rewrite split_sum_mt /is_pad. iExists i. rewrite nth_lookup Hty. iFrame.
     iSplitL "H↦pad".
     - rewrite (shift_loc_assoc_nat _ 1) take_length Nat.min_l; last lia.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 6ec339ef2ed195b9cf874e698d84b11b47f93d30..0c747e2984f26649c985878a69f574a242674d81 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -44,25 +44,40 @@ Section uniq_bor.
   Global Instance uniq_bor_wf κ ty `{!TyWf ty} : TyWf (uniq_bor κ ty) :=
     { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty κ }.
 
-  Global Instance uniq_mono E L :
-    Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) uniq_bor.
+  Lemma uniq_type_incl κ1 κ2 ty1 ty2 :
+    κ2 ⊑ κ1 -∗
+    ▷ type_equal ty1 ty2 -∗
+    type_incl (uniq_bor κ1 ty1) (uniq_bor κ2 ty2).
   Proof.
-    intros κ1 κ2 Hκ ty1 ty2. rewrite eqtype_unfold=>Hty. iIntros (?) "HL".
-    iDestruct (Hty with "HL") as "#Hty". iDestruct (Hκ with "HL") as "#Hκ".
-    iIntros "!# #HE". iSplit; first done.
-    iDestruct ("Hty" with "HE") as "(_ & #Ho & #Hs)"; [done..|clear Hty].
-    iSpecialize ("Hκ" with "HE"). iSplit; iModIntro.
+    iIntros "#Hlft #Hty". iSplit; first done.
+    iSplit; iModIntro.
     - iIntros (? [|[[]|][]]) "H"; try done.
-      iApply (bor_shorten with "Hκ"). iApply bor_iff; last done.
-      iNext. iModIntro. iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
-      iExists vl; iFrame; by iApply "Ho".
+      iApply (bor_shorten with "Hlft"). iApply bor_iff; last done.
+      iNext. iModIntro.
+      iDestruct "Hty" as "(_ & Hty & _)".
+      iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
+      iExists vl; iFrame; by iApply "Hty".
     - iIntros (κ ??) "H". iAssert (κ2 ⊓ κ ⊑ κ1 ⊓ κ)%I as "#Hincl'".
-      { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
+      { iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
       iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'. iIntros "{$Hbor}!# %%% Htok".
       iMod (lft_incl_acc with "Hincl' Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
       iMod ("Hupd" with "[%] Htok") as "Hupd'"; try done. iModIntro. iNext.
       iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
-      iApply ty_shr_mono; [done..|]. by iApply "Hs".
+      iDestruct "Hty" as "(_ & _ & Hty)".
+      iApply ty_shr_mono; last by iApply "Hty".
+      done.
+  Qed.
+
+  Global Instance uniq_mono E L :
+    Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) uniq_bor.
+  Proof.
+    intros κ1 κ2 Hκ ty1 ty2. rewrite eqtype_unfold=>Hty. iIntros (??) "HL".
+    iDestruct (Hty with "HL") as "#Hty". iDestruct (Hκ with "HL") as "#Hκ".
+    iIntros "!# #HE".
+    iApply uniq_type_incl.
+    - iDestruct ("Hκ" with "HE") as %H.
+      apply lft_incl_syn_sem in H. iApply H.
+    - iNext. iApply "Hty". done.
   Qed.
   Global Instance uniq_mono_flip E L :
     Proper (lctx_lft_incl E L ==> eqtype E L ==> flip (subtype E L)) uniq_bor.
@@ -112,7 +127,8 @@ Section typing.
     lctx_lft_incl E L κ' κ →
     tctx_incl E L [p ◁ &uniq{κ}ty] [p ◁ &uniq{κ'}ty; p ◁{κ'} &uniq{κ}ty].
   Proof.
-    iIntros (Hκκ' tid ?) "#LFT HE HL H". iDestruct (Hκκ' with "HL HE") as "#Hκκ'".
+    iIntros (Hκκ' tid ??) "#LFT HE HL H". iDestruct (Hκκ' with "HL HE") as %H.
+    iDestruct (lft_incl_syn_sem κ' κ H) as "Hκκ'".
     iFrame. rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as ([[]|]) "[% Hb]"; try done.
     iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]". done. iModIntro.
@@ -132,7 +148,7 @@ Section typing.
     Copy ty → lctx_lft_alive E L κ → ⊢ typed_read E L (&uniq{κ}ty) ty (&uniq{κ}ty).
   Proof.
     rewrite typed_read_eq. iIntros (Hcopy Halive) "!#".
-    iIntros ([[]|] tid F qL ?) "#LFT #HE Htl HL Hown"; try done.
+    iIntros ([[]|] tid F qmax qL ?) "#LFT #HE Htl HL Hown"; try done.
     iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first solve_ndisj.
     iMod (bor_acc with "LFT Hown Hκ") as "[H↦ Hclose']"; first solve_ndisj.
     iDestruct "H↦" as (vl) "[>H↦ #Hown]".
@@ -146,7 +162,7 @@ Section typing.
     lctx_lft_alive E L κ → ⊢ typed_write E L (&uniq{κ}ty) ty (&uniq{κ}ty).
   Proof.
     rewrite typed_write_eq. iIntros (Halive) "!#".
-    iIntros ([[]|] tid F qL ?) "#LFT HE HL Hown"; try done.
+    iIntros ([[]|] tid F qmax qL ?) "#LFT HE HL Hown"; try done.
     iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
     iMod (bor_acc with "LFT Hown Htok") as "[H↦ Hclose']"; first solve_ndisj.
     iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).