diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 238300b5e2fa8cb5a01ba774fe0146d270539a57..6ad7b8d070e30ba9b86a224c1f15303fb68aeff2 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -300,6 +300,7 @@ Arguments lctx_lft_incl {_ _ _} _%EL _%LL _ _.
 Arguments lctx_lft_eq {_ _ _} _%EL _%LL _ _.
 Arguments lctx_lft_alive {_ _ _} _%EL _%LL _.
 Arguments elctx_sat {_ _ _} _%EL _%LL _%EL.
+Arguments lctx_lft_alive_tok {_ _ _ _%EL _%LL} _ _ _.
 
 Lemma elctx_sat_cons_weaken `{invG Σ, lftG Σ} e0 E E' L :
   elctx_sat E L E' → elctx_sat (e0 :: E) L E'.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 4a3cacb5ad40b91db922e148f6ff33eeac95fb19..06c092adf1b1337d05d378263332ad861e949e84 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -160,7 +160,7 @@ Section typing.
     iIntros "(Hr & Hc & #Hc' & Hx)".
     destruct c' as [[|c'|]|]; try done. destruct x as [[|x|]|]; try done.
     destruct r as [[|r|]|]; try done.
-    iMod (lctx_lft_alive_tok _ _ α with "HE HL") as (q') "(Htok & HL & Hclose1)"; [solve_typing..|].
+    iMod (lctx_lft_alive_tok α with "HE HL") as (q') "(Htok & HL & Hclose1)"; [solve_typing..|].
     iMod (na_bor_acc with "LFT Hc' Htok Htl") as "(Hc'↦ & Htl & Hclose2)"; [solve_ndisj..|].
     iDestruct "Hc'↦" as (vc') "[>Hc'↦ Hc'own]".
     iDestruct (ty_size_eq with "Hc'own") as "#>%".
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index 79c1b44cbacb9bf33ced19da089b4867878a39e0..09f45a8883e4aff86136edcdfabb8f9c5881e202 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -241,7 +241,7 @@ Section code.
     iDestruct (ownptr_uninit_own with "Hrc2") as (lrc2 vlrc2) "(% & Hrc2 & Hrc2†)".
     subst rc2. inv_vec vlrc2=>rc2. rewrite heap_mapsto_vec_singleton.
     (* All right, we are done preparing our context. Let's get going. *)
-    iMod (lctx_lft_alive_tok _ _ α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
+    iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
     wp_bind (!_)%E.
     iSpecialize ("Hshr" with "[] Hα1"); last iApply (wp_step_fupd with "Hshr"); [done..|].
     iMod (frac_bor_acc with "LFT Hlrc Hα2") as (q') "[Hlrc↦ Hclose]"; first solve_ndisj.
@@ -300,7 +300,7 @@ Section code.
     destruct rc' as [[|rc'|]|]; try done. simpl of_val.
     iDestruct "Hrc'" as (l') "[#Hrc' #Hdelay]".
     (* All right, we are done preparing our context. Let's get going. *)
-    iMod (lctx_lft_alive_tok _ _ α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
+    iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
     wp_bind (!_)%E.
     iSpecialize ("Hdelay" with "[] Hα1"); last iApply (wp_step_fupd with "Hdelay"); [done..|].
     iMod (frac_bor_acc with "LFT Hrc' Hα2") as (q') "[Hrc'↦ Hclose2]"; first solve_ndisj.
@@ -490,7 +490,7 @@ Section code.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hx _]]]".
     rewrite !tctx_hasty_val  [[rcx]]lock [[x]]lock.
     destruct rc' as [[|rc'|]|]; try done.
-    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 & Hclose1)"; [solve_typing..|].
     iMod (bor_acc_cons with "LFT Hrc' Hα") as "[Hrc' Hclose2]"; first solve_ndisj.
     iDestruct (heap_mapsto_ty_own with "Hrc'") as (vl) "[>Hrc' Hrcown]".
     inv_vec vl=>l. rewrite heap_mapsto_vec_singleton.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index edf3b5b14cdce6404df4ca1bde27c9d4a064ad3b..e71822aeeae6bce95fef5cce9c7949a024bfd486 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -69,10 +69,10 @@ Typeclasses Opaque llctx_interp.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
     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 (lctx_lft_alive_tok _ _ α with "HE HL") as (qα) "(Hα & HL & Hclose')";
-      [solve_typing..|].
+    iMod (lctx_lft_alive_tok β with "HE HL") as (qβ) "(Hβ & HL & Hclose)"; [solve_typing..|].
     iMod (lft_incl_acc with "Hβδ Hβ") as (qδ) "[Hδ Hcloseβ]". done.
+    iMod (lctx_lft_alive_tok α 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..|].
     iMod (na_bor_acc with "LFT H◯inv Hα2 Hna") as "(H◯ & Hna & Hcloseα2)"; [solve_ndisj..|].
@@ -93,20 +93,20 @@ Typeclasses Opaque llctx_interp.
     iAssert (lx' ↦∗{qlx'} [ #lv; #lrc])%I  with "[H↦1 H↦2]" as "H↦".
     { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
     wp_let. wp_apply (wp_memcpy with "[$Hlr $H↦]"); [done..|].
-    iIntros "[Hlr H↦]". wp_seq. iMod ("Hcloseα2" with "[$H◯] Hna") as "[Hα2 Hna]".
+    iIntros "[Hlr H↦]". wp_seq. iMod ("Hcloseα2" with "[$H◯] Hna") as "[Hα1 Hna]".
     iMod ("Hcloseδ" with "[H↦lrc H● Hν1 Hshr' H†] Hna") as "[Hδ Hna]".
     { iExists _. rewrite Z.add_comm. iFrame. iExists _. iFrame. iSplitR.
       - rewrite /= agree_idemp. auto.
       - iExists _. iFrame.
         rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto. }
-    iMod ("Hcloseβ" with "Hδ") as "Hβ". iMod ("Hcloseα1" with "[$H↦]") as "Hα1".
+    iMod ("Hcloseβ" with "Hδ") as "Hβ". iMod ("Hcloseα1" with "[$H↦]") as "Hα2".
+    iMod ("Hclose'" with "[$Hα1 $Hα2] HL") as "HL". iMod ("Hclose" with "Hβ HL") as "HL".
     iApply (type_type _ _ _
            [ x ◁ box (&shr{α} ref β ty); #lr ◁ box(ref β ty)]%TC
-        with "[] LFT Hna [Hα1 Hα2 Hβ] HL Hk"); first last.
+        with "[] LFT HE Hna HL Hk"); first last.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       rewrite /= freeable_sz_full. iFrame. iExists _. iFrame. iExists _, _, _, _, _.
       iFrame "∗#". }
-    { rewrite /elctx_interp big_sepL_cons big_sepL_singleton. iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
@@ -121,27 +121,27 @@ Typeclasses Opaque llctx_interp.
 
   Lemma ref_deref_type ty :
     typed_val ref_deref
-      (fn (fun '(α, β) => FP [α; β; α ⊑ β]%EL [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T)).
+      (fn (fun '(α, β) => FP (λ ϝ, [ϝ ⊑ α; α ⊑ β]%EL)
+                             [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
+      iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
-    iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
     iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hx')".
-    rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
-    iDestruct "HE" as "(Hα & Hβ & #Hαβ)".
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
     iMod (frac_bor_acc with "LFT Hfrac Hα") as (qlx') "[H↦ Hcloseα]". done.
     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↦1 $H↦2]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
     iApply (type_type _ _ _
         [ x ◁ box (&shr{α} ref β ty); #lv ◁ &shr{α}ty]%TC
-        with "[] LFT Hna [Hα Hβ Hαβ] HL Hk"); first last.
+        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. }
-    { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
+      iFrame. iApply (ty_shr_mono with "[] Hshr"). iApply lft_incl_glb; last done.
+      rewrite /elctx_interp. iDestruct "HE" as "(_ & $ & _)". }
     iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -158,17 +158,17 @@ Typeclasses Opaque llctx_interp.
       let: "r" := new [ #0] in return: ["r"].
 
   Lemma ref_drop_type ty :
-    typed_val ref_drop (fn(∀ α, [α]; ref α ty) → unit).
+    typed_val ref_drop (fn(∀ α, (λ ϝ, [ϝ ⊑ α]); ref α ty) → unit).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
-    iIntros (tid qE) "#LFT Hna Hα HL Hk Hx".
-    rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_singleton tctx_hasty_val.
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk Hx". rewrite tctx_interp_singleton tctx_hasty_val.
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
     iDestruct "Hx" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hx"; try iDestruct "Hx" as "[_ >[]]".
     rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
     iDestruct "Hx" as "[[Hx↦1 Hx↦2] Hx]". wp_op. wp_read. wp_let.
     iDestruct "Hx" as (ν q γ β ty') "(_ & #Hαβ & #Hinv & Hν & H◯)".
+    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 (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hcloseβ)"; [done..|].
     iDestruct (refcell_inv_reading_inv with "INV [$Hâ—¯]")
@@ -197,12 +197,11 @@ Typeclasses Opaque llctx_interp.
     wp_bind Endlft. iApply (wp_mask_mono (↑lftN)); first done.
     iApply (wp_step_fupd with "INV"); [set_solver..|]. wp_seq.
     iIntros "INV !>". wp_seq. iMod ("Hcloseβ" with "[$INV] Hna") as "[Hβ Hna]".
-    iMod ("Hcloseα" with "Hβ") as "Hα".
-    iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)]%TC with "[] LFT Hna [Hα] HL Hk");
+    iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)]%TC with "[] LFT HE Hna HL Hk");
       first last.
     { rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame. iExists [ #lv;#lrc].
       rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton uninit_own. iFrame. auto. }
-    { by rewrite /elctx_interp big_sepL_singleton. }
     iApply type_delete; [solve_typing..|].
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_jump; solve_typing.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 5451b568d531047c288ae4de375477f0d6929ce3..eb8c30909b5048767ac7fdbf31923eeb9f08771b 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -20,12 +20,12 @@ Section refcell_functions.
       delete [ #ty.(ty_size) ; "x"];; return: ["r"].
 
   Lemma refcell_new_type ty :
-    typed_val (refcell_new ty) (fn([]; ty) → refcell ty).
+    typed_val (refcell_new ty) (fn(λ ϝ, []; ty) → refcell ty).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
+      iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|].
-    iIntros (r tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+    iIntros (r tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
     rewrite (Nat2Z.id (S ty.(ty_size))) tctx_interp_cons
             tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hr Hx]".
@@ -36,7 +36,7 @@ Section refcell_functions.
     wp_apply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [by auto using vec_to_list_length..|].
     iIntros "[Hr↦1 Hx↦]". wp_seq.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lr ◁ box (refcell ty)]%TC
-        with "[] LFT Hna HE HL Hk [-]"); last first.
+        with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
       iSplitL "Hx↦".
       - iExists _. rewrite uninit_own. auto.
@@ -55,12 +55,12 @@ Section refcell_functions.
        delete [ #(S ty.(ty_size)) ; "x"];; return: ["r"].
 
   Lemma refcell_into_inner_type ty :
-    typed_val (refcell_into_inner ty) (fn([]; refcell ty) → ty).
+    typed_val (refcell_into_inner ty) (fn(λ ϝ, []; refcell ty) → ty).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
+      iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|].
-    iIntros (r tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+    iIntros (r tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
     rewrite (Nat2Z.id (ty.(ty_size))) tctx_interp_cons
             tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hr Hx]".
@@ -72,7 +72,7 @@ Section refcell_functions.
     wp_op. wp_apply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [by auto using vec_to_list_length..|].
     iIntros "[Hr↦ Hx↦1]". wp_seq.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (S (ty_size ty))); #lr ◁ box ty]%TC
-        with "[] LFT Hna HE HL Hk [-]"); last first.
+        with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iSplitR "Hr↦ Hx".
       - iExists (_::_). rewrite heap_mapsto_vec_cons uninit_own. iFrame.
@@ -89,12 +89,13 @@ Section refcell_functions.
       return: ["x"].
 
   Lemma refcell_get_mut_type ty :
-    typed_val refcell_get_mut (fn(∀ α, [α]; &uniq{α} (refcell ty)) → &uniq{α} ty)%T.
+    typed_val refcell_get_mut
+             (fn(∀ α, λ ϝ, [ϝ ⊑ α]; &uniq{α} (refcell ty)) → &uniq{α} ty)%T.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
-    iIntros (tid qE) "#LFT Hna HE HL HC HT".
+    iIntros (tid) "#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⌝) ∗
@@ -110,7 +111,7 @@ Section refcell_functions.
     iDestruct "Hx" as (vl) "[Hx↦ Hx]". rewrite uninit_own. wp_op.
     iApply (type_type _ _ _
             [ #lx ◁ box (uninit 1); #(shift_loc lx' 1) ◁ &uniq{α}ty]%TC
-            with "[] LFT Hna HE HL HC [-]"); last first.
+            with "[] LFT HE Hna HL HC [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iNext. iExists _. rewrite uninit_own. iFrame. }
     iApply type_assign; [solve_typing..|].
@@ -139,32 +140,34 @@ Section refcell_functions.
       delete [ #1; "x"];; return: ["r"].
 
   Lemma refcell_try_borrow_type ty :
-    typed_val refcell_try_borrow (fn(∀ α, [α] ; &shr{α}(refcell ty)) → option (ref α ty)).
+    typed_val refcell_try_borrow
+      (fn(∀ α, λ ϝ, [ϝ ⊑ α] ; &shr{α}(refcell ty)) → option (ref α ty)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
-    iApply (type_cont [] [] (λ _, [x ◁ box (&shr{α} refcell ty);
-                                    r ◁ box (option (ref α ty))])%TC);
+    iApply (type_cont [] [ϝ ⊑ []]%LL (λ _, [x ◁ box (&shr{α} refcell ty);
+                                         r ◁ box (option (ref α ty))])%TC);
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg]; simpl_subst; last first.
     { iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing. }
     iApply type_deref; [solve_typing..|].
-    iIntros (x' tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+    iIntros (x' tid) "#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]".
-    rewrite {1}/elctx_interp big_sepL_singleton.
-    iMod (lft_incl_acc with "Hαβ HE") as (qβ) "[[Hβtok1 Hβtok2] Hclose]". done.
-    iMod (na_bor_acc with "LFT Hinv Hβtok1 Hna") as "(INV & Hna & Hclose')"; try done.
+    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βtok1 Hβtok2] Hclose']". done.
+    iMod (na_bor_acc with "LFT Hinv Hβtok1 Hna") as "(INV & Hna & Hclose'')"; try done.
     iDestruct "INV" as (st) "(Hlx & Hownst & Hst)". wp_read. wp_let. wp_op=>?; wp_if.
-    - iMod ("Hclose'" with "[Hlx Hownst Hst] Hna") as "[Hβtok1 Hna]";
+    - iMod ("Hclose''" with "[Hlx Hownst Hst] Hna") as "[Hβtok1 Hna]";
         first by iExists st; iFrame.
+      iMod ("Hclose'" with "[$Hβtok1 $Hβtok2]") as "Hα".
+      iMod ("Hclose" with "Hα HL") as "HL".
       iApply (type_type _ _ _
               [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3) ]%TC
-              with "[] LFT Hna [> Hclose Hβtok1 Hβtok2] HL Hk"); first last.
+              with "[] LFT HE Hna HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
-      { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_unit (option $ ref α ty)); [solve_typing..|]; first last.
       simpl. iApply type_jump; solve_typing.
     - wp_op. wp_write. wp_apply wp_new; [done..|].
@@ -206,17 +209,17 @@ Section refcell_functions.
           + iIntros "!> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro.
             iNext. iMod "Hν". iApply "Hh". rewrite -lft_dead_or. auto.
           + iExists _. iFrame. by rewrite Qp_div_2. }
-      iMod ("Hclose'" with "[$INV] Hna") as "[Hβtok1 Hna]".
+      iMod ("Hclose''" with "[$INV] Hna") as "[Hβtok1 Hna]".
+      iMod ("Hclose'" with "[$Hβtok1 $Hβtok2]") as "Hα".
+      iMod ("Hclose" with "Hα HL") as "HL".
       iApply (type_type  _ _ _
         [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3); #lref ◁ box (ref α ty)]%TC
-              with "[] LFT Hna [> Hclose Hβtok1 Hβtok2] HL Hk");
-        first last.
+              with "[] LFT HE Hna HL Hk"); first last.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
         rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
         iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
         iFrame. iExists _, _, _, _, _. iFrame "∗#". iApply ty_shr_mono; try by auto.
         iApply lft_intersect_mono. done. iApply lft_incl_refl. }
-      { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_memcpy (option $ ref α ty)); [solve_typing..|].
       simpl. iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing.
@@ -245,25 +248,25 @@ Section refcell_functions.
 
   Lemma refcell_try_borrow_mut_type ty :
     typed_val refcell_try_borrow_mut
-              (fn(∀ α, [α]; &shr{α}(refcell ty)) → option (refmut α ty))%T.
+              (fn(∀ α, λ ϝ, [ϝ ⊑ α]; &shr{α}(refcell ty)) → option (refmut α ty))%T.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
-    iApply (type_cont [] [] (λ _, [x ◁ box (&shr{α} refcell ty);
-                                    r ◁ box (option (refmut α ty))]%TC));
+    iApply (type_cont [] [ϝ ⊑ []]%LL (λ _, [x ◁ box (&shr{α} refcell ty);
+                                            r ◁ box (option (refmut α ty))]%TC));
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg];
       simpl_subst; last first.
     { iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing. }
     iApply type_deref; [solve_typing..|].
-    iIntros (x' tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+    iIntros (x' tid) "#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]".
-    rewrite {1}/elctx_interp big_sepL_singleton.
-    iMod (lft_incl_acc with "Hαβ HE") as (qβ) "[Hβtok Hclose]". done.
-    iMod (na_bor_acc with "LFT Hinv Hβtok Hna") as "(INV & Hna & Hclose')"; try done.
+    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βtok Hclose']". done.
+    iMod (na_bor_acc with "LFT Hinv Hβtok Hna") as "(INV & Hna & Hclose'')"; try done.
     iDestruct "INV" as (st) "(Hlx & Hownst & Hb)". wp_read. wp_let. wp_op=>?; wp_if.
     - wp_write. wp_apply wp_new; [done..|].
       iIntros (lref vl) "(EQ & H† & Hlref)". iDestruct "EQ" as %?%(inj Z.of_nat 2%nat).
@@ -277,29 +280,29 @@ Section refcell_functions.
       iApply fupd_wp. iApply (fupd_mask_mono (↑lftN)); first done.
       iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hb") as "[Hb Hbh]". done.
       { iApply lft_intersect_incl_l. }
-      iModIntro. iMod ("Hclose'" with "[Hlx Hownst Hbh] Hna") as "[Hβtok Hna]".
+      iModIntro. iMod ("Hclose''" with "[Hlx Hownst Hbh] Hna") as "[Hβtok Hna]".
       { iExists _. iFrame. iExists ν. iSplit; first by auto. iNext. iSplitL; last by auto.
         iIntros "Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
         iApply "Hbh". rewrite -lft_dead_or. auto. }
+      iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
       iApply (type_type _ _ _
         [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3); #lref ◁ box (refmut α ty)]%TC
-              with "[] LFT Hna [> Hclose Hβtok] HL Hk"); first last.
+              with "[] LFT HE Hna HL Hk"); first last.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
         rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
         iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
         iFrame. iExists _, _, _, _. iFrame "#∗". iApply (bor_shorten with "[] [$Hb]").
         iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
-      { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_memcpy (option $ refmut α ty)); [solve_typing..|].
       simpl. iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing.
-    - iMod ("Hclose'" with "[Hlx Hownst Hb] Hna") as "[Hβtok Hna]";
+    - iMod ("Hclose''" with "[Hlx Hownst Hb] Hna") as "[Hβtok Hna]";
         first by iExists st; iFrame.
+      iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
       iApply (type_type _ _ _
               [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3) ]%TC
-              with "[] LFT Hna [> Hclose Hβtok] HL Hk"); first last.
+              with "[] LFT HE Hna HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
-      { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_unit (option $ refmut α ty)); [solve_typing..|].
       simpl. iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index a1d838cf20bd095db614e83f800d845c75349339..af9e25bed470a78bf6bec7126b84abbd50225300 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -20,31 +20,34 @@ Section refmut_functions.
 
   Lemma refmut_deref_type ty :
     typed_val refmut_deref
-      (fn (fun '(α, β) => FP [α; β; α ⊑ β]%EL [# &shr{α}(refmut β ty)]%T (&shr{α}ty))).
+      (fn (fun '(α, β) => FP (λ ϝ, [ϝ ⊑ α; α ⊑ β]%EL)
+                             [# &shr{α}(refmut β ty)]%T (&shr{α}ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
+      iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
-    iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
     iDestruct "Hx'" as (lv lrc) "#(Hfrac & #Hshr)".
-    rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
-    iDestruct "HE" as "([Hα1 Hα2] & Hβ & #Hαβ)".
+    iMod (lctx_lft_alive_tok α 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.
     rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+    iMod (lctx_lft_alive_tok β 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β]");
          [done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
     iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β] !>". wp_let.
     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".
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} refmut β ty); #lv ◁ &shr{α}ty]%TC
-            with "[] LFT Hna [Hα1 Hα2 Hβ Hαβ] HL Hk"); last first.
+            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.
-      iApply lft_incl_refl. }
-    { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
+      iFrame. iApply (ty_shr_mono with "[] Hshr'").
+      iApply lft_incl_glb; last iApply lft_incl_refl. iDestruct "HE" as "(_ & $ & _)". }
     iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -60,19 +63,19 @@ Section refmut_functions.
 
   Lemma refmut_derefmut_type ty :
     typed_val refmut_derefmut
-      (fn (fun '(α, β) => FP [α; β; α ⊑ β]%EL [# &uniq{α}(refmut β ty)]%T
+      (fn (fun '(α, β) => FP (λ ϝ, [ϝ ⊑ α; α ⊑ β]%EL) [# &uniq{α}(refmut β ty)]%T
                               (&uniq{α}ty)%T)).
    Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
+      iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
-    iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-    iDestruct "HT" as "[Hx Hx']".
-    rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
-    iDestruct "HE" as "(Hα & Hβ & #Hαβ)". destruct x' as [[|lx'|]|]; try done.
+    iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
     iMod (bor_exists with "LFT Hx'") as (vl) "H". done.
     iMod (bor_sep with "LFT H") as "[H↦ H]". done.
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose')";
+      [solve_typing..|].
     destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
       try by iMod (bor_persistent_tok with "LFT H Hα") as "[>[] _]".
     iMod (bor_exists with "LFT H") as (ν) "H". done.
@@ -92,13 +95,13 @@ Section refmut_functions.
     wp_bind (!(LitV lx'))%E. iApply (wp_step_fupd with "[Hb]");
       [done| |by iApply (bor_unnest with "LFT Hb")|]; first done.
     wp_read. iIntros "Hb !>". wp_let.
-    iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]".
+    iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]". iMod ("Hclose'" with "Hα HL") as "HL".
     iApply (type_type _ _ _ [ x ◁ box (uninit 1); #lv ◁ &uniq{α}ty]%TC
-            with "[] LFT Hna [Hα Hβ Hαβ] HL Hk"); last first.
+            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]. }
-    { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
+      iApply lft_incl_glb; [iApply lft_incl_glb|iApply lft_incl_refl]; last done.
+      iDestruct "HE" as "(_ & $ & _)". }
     iApply (type_letalloc_1 (&uniq{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -114,17 +117,18 @@ Section refmut_functions.
       let: "r" := new [ #0] in return: ["r"].
 
   Lemma refmut_drop_type ty :
-    typed_val refmut_drop (fn(∀ α, [α]; refmut α ty) → unit).
+    typed_val refmut_drop (fn(∀ α, (λ ϝ, [ϝ ⊑ α]); refmut α ty) → unit).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
-    iIntros (tid qE) "#LFT Hna Hα HL Hk Hx".
-    rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_singleton tctx_hasty_val.
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk Hx". rewrite tctx_interp_singleton tctx_hasty_val.
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
     iDestruct "Hx" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hx"; try iDestruct "Hx" as "[_ >[]]".
     rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
     iDestruct "Hx" as "[[Hx↦1 Hx↦2] Hx]". wp_op. wp_read. wp_let.
     iDestruct "Hx" as (ν γ β ty') "(Hb & #Hαβ & #Hinv & Hν & H◯)".
+    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 (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hcloseβ)"; [done..|].
     iDestruct "INV" as (st) "(H↦lrc & H● & INV)". wp_write.
@@ -142,12 +146,11 @@ Section refmut_functions.
     { iExists None. iFrame. iMod (own_update_2 with "H● H◯") as "$"; last done.
       apply auth_update_dealloc. rewrite -(right_id None _ (Some _)).
       apply cancel_local_update_empty, _. }
-    iMod ("Hcloseα" with "Hβ") as "Hα". wp_seq.
+    iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL". wp_seq.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)]%TC
-            with "[] LFT Hna [Hα] HL Hk"); last first.
+            with "[] LFT HE Hna HL Hk"); last first.
     { rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame. iExists [ #lv;#lrc].
       rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton uninit_own. iFrame. auto. }
-    { by rewrite /elctx_interp big_sepL_singleton. }
     iApply type_delete; [solve_typing..|].
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_jump; solve_typing.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 049e5ce511eff50838d2077d003f0fa272fb9c19..fe5b772d78f3298c20df8e316ad44baefa6bc2f1 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -58,17 +58,18 @@ Section rwlock_inv.
     intros n ???. eapply rwlock_inv_type_ne, type_dist_dist2. done.
   Qed.
 
-  Lemma rwlock_inv_proper E L tid l γ α ty1 ty2 :
+  Lemma rwlock_inv_proper E L ty1 ty2 q :
     eqtype E L ty1 ty2 →
-    elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
-    rwlock_inv tid l γ α ty1 -∗ rwlock_inv tid l γ α ty2.
+    llctx_interp L q -∗ ∀ tid l γ α, □ (elctx_interp E -∗
+    rwlock_inv tid l γ α ty1 -∗ rwlock_inv tid l γ α ty2).
   Proof.
     (* TODO : this proof is essentially [solve_proper], but within the logic.
               It would easily gain from some automation. *)
-    iIntros (Hty%eqtype_unfold) "#HE #HL H". unfold rwlock_inv.
-    iDestruct (Hty with "HE HL") as "(% & Hown & Hshr)".
+    rewrite eqtype_unfold. iIntros (Hty) "HL".
+    iDestruct (Hty with "HL") as "#Hty". iIntros "* !# #HE H".
+    iDestruct ("Hty" with "HE") as "(% & #Hown & #Hshr)".
     iAssert (□ (&{α} shift_loc l 1 ↦∗: ty_own ty1 tid -∗
-                &{α} shift_loc l 1 ↦∗: ty_own ty2 tid))%I with "[]" as "#Hb".
+                &{α} shift_loc l 1 ↦∗: ty_own ty2 tid))%I as "#Hb".
     { iIntros "!# H". iApply bor_iff; last done.
       iSplit; iIntros "!>!#H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
       iFrame; by iApply "Hown". }
@@ -164,14 +165,17 @@ 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) "#HE #HL". pose proof EQ as EQ'%eqtype_unfold.
-    iDestruct (EQ' with "HE HL") as "(% & #Hown & #Hshr)".
+    iIntros (ty1 ty2 EQ 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.
+    iIntros "!# #HE". iDestruct ("EQ'" with "HE") as "(% & #Hown & #Hshr)".
     iSplit; [|iSplit; iIntros "!# * H"].
     - iPureIntro. simpl. congruence.
     - destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ H]". by iApply "Hown".
     - iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
-      iApply shr_bor_iff; last done.
-      iSplit; iIntros "!>!# H"; by iApply rwlock_inv_proper.
+      iApply shr_bor_iff; last done. iSplit; iIntros "!>!# H".
+      by iApply "Hty1ty2". by iApply "Hty2ty1".
   Qed.
   Lemma rwlock_mono' E L ty1 ty2 :
     eqtype E L ty1 ty2 → subtype E L (rwlock ty1) (rwlock ty2).
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 393e673f57fd86331bb5502481e1bfbbb7d9b7a0..408778d961dc465402d8b344cf0dc80407125b2b 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -20,12 +20,12 @@ Section rwlock_functions.
        delete [ #ty.(ty_size) ; "x"];; return: ["r"].
 
   Lemma rwlock_new_type ty :
-    typed_val (rwlock_new ty) (fn([]; ty) → rwlock ty).
+    typed_val (rwlock_new ty) (fn(λ ϝ, []; ty) → rwlock ty).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
+      iIntros (_ ret ϝ arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|].
-    iIntros (r tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+    iIntros (r tid) "#LFT HE Hna HL Hk HT". simpl_subst.
     rewrite (Nat2Z.id (S ty.(ty_size))) tctx_interp_cons
             tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try done.
@@ -38,7 +38,7 @@ Section rwlock_functions.
     wp_apply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [done||lia..|].
     iIntros "[Hr↦1 Hx↦]". wp_seq.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lr ◁ box (rwlock ty)]%TC
-        with "[] LFT Hna HE HL Hk [-]"); last first.
+        with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
       iSplitL "Hx↦".
       - iExists _. rewrite uninit_own. auto.
@@ -56,12 +56,12 @@ Section rwlock_functions.
        delete [ #(S ty.(ty_size)) ; "x"];; return: ["r"].
 
   Lemma rwlock_into_inner_type ty :
-    typed_val (rwlock_into_inner ty) (fn([] ; rwlock ty) → ty).
+    typed_val (rwlock_into_inner ty) (fn(λ ϝ, [] ; rwlock ty) → ty).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
+      iIntros (_ ret ϝ arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|].
-    iIntros (r tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+    iIntros (r tid) "#LFT HE Hna HL Hk HT". simpl_subst.
     rewrite (Nat2Z.id (ty.(ty_size))) tctx_interp_cons
             tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try done.
@@ -74,7 +74,7 @@ Section rwlock_functions.
     wp_apply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [done||lia..|].
     iIntros "[Hr↦ Hx↦1]". wp_seq.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (S (ty_size ty))); #lr ◁ box ty]%TC
-        with "[] LFT Hna HE HL Hk [-]"); last first.
+        with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iSplitR "Hr↦ Hx".
       - iExists (_::_). rewrite heap_mapsto_vec_cons uninit_own -Hsz. iFrame. auto.
@@ -90,12 +90,12 @@ Section rwlock_functions.
       return: ["x"].
 
   Lemma rwlock_get_mut_type ty :
-    typed_val rwlock_get_mut (fn(∀ α, [α]; &uniq{α} (rwlock ty)) → &uniq{α} ty).
+    typed_val rwlock_get_mut (fn(∀ α, λ ϝ, [ϝ ⊑ α]; &uniq{α} (rwlock ty)) → &uniq{α} ty).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
-    iIntros (tid qE) "#LFT Hna HE HL HC HT".
+    iIntros (tid) "#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⌝) ∗
@@ -111,7 +111,7 @@ Section rwlock_functions.
     iDestruct "Hx" as (vl) "[Hx↦ Hx]". rewrite uninit_own. wp_op.
     iApply (type_type _ _ _
             [ #lx ◁ box (uninit 1); #(shift_loc lx' 1) ◁ &uniq{α}ty]%TC
-            with "[] LFT Hna HE HL HC [-]"); last first.
+            with "[] LFT HE Hna HL HC [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iNext. iExists _. rewrite uninit_own. iFrame. }
     iApply type_assign; [solve_typing..|].
@@ -141,43 +141,44 @@ Section rwlock_functions.
 
   Lemma rwlock_try_read_type ty :
     typed_val rwlock_try_read
-        (fn(∀ α, [α]; &shr{α}(rwlock ty)) → option (rwlockreadguard α ty)).
+        (fn(∀ α, λ ϝ, [ϝ ⊑ α]; &shr{α}(rwlock ty)) → option (rwlockreadguard α ty)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
-    iApply (type_cont [] [] (λ _, [x ◁ box (&shr{α} rwlock ty);
-                                   r ◁ box (option (rwlockreadguard α ty))])%TC);
+    iApply (type_cont [] [ϝ ⊑ []]%LL (λ _, [x ◁ box (&shr{α} rwlock ty);
+                                            r ◁ box (option (rwlockreadguard α ty))])%TC);
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg];
       simpl_subst; last first.
     { iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing. }
-    iApply (type_cont [] [] (λ _, [x ◁ _; x' ◁ _; r ◁ _])%TC);
+    iApply (type_cont [] [ϝ ⊑ []]%LL (λ _, [x ◁ _; x' ◁ _; r ◁ _])%TC);
       [iIntros (loop)|iIntros "/= !#"; iIntros (loop arg); inv_vec arg];
       simpl_subst.
     { iApply type_jump; solve_typing. }
-    iIntros (tid qE) "#LFT Hna HE HL Hk HT".
+    iIntros (tid) "#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]".
-    rewrite {1}/elctx_interp big_sepL_singleton.
-    iMod (lft_incl_acc with "Hαβ HE") as (qβ) "[[Hβtok1 Hβtok2] Hclose]". done.
+    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βtok1 Hβtok2] Hclose']". done.
     wp_bind (!ˢᶜ(LitV lx))%E.
-    iMod (shr_bor_acc_tok with "LFT Hinv Hβtok1") as "[INV Hclose']"; try done.
+    iMod (shr_bor_acc_tok with "LFT Hinv Hβtok1") as "[INV Hclose'']"; try done.
     iDestruct "INV" as (st) "(Hlx & INV)". wp_read.
-    iMod ("Hclose'" with "[Hlx INV]") as "Hβtok1"; first by iExists _; iFrame.
+    iMod ("Hclose''" with "[Hlx INV]") as "Hβtok1"; first by iExists _; iFrame.
     iModIntro. wp_let. wp_op=>Hm1; wp_if.
-    - iApply (type_type _ _ _
+    - iMod ("Hclose'" with "[$]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+      iApply (type_type _ _ _
               [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2) ]%TC
-              with "[] LFT Hna [> Hclose Hβtok1 Hβtok2] HL Hk"); first last.
+              with "[] LFT HE Hna HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
-      { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_unit (option $ rwlockreadguard α ty));
         [solve_typing..|]; first last.
       simpl. iApply type_jump; solve_typing.
     - wp_op. wp_bind (CAS _ _ _).
-      iMod (shr_bor_acc_tok with "LFT Hinv Hβtok1") as "[INV Hclose']"; try done.
+      iMod (shr_bor_acc_tok with "LFT Hinv Hβtok1") as "[INV Hclose'']"; try done.
       iDestruct "INV" as (st') "(Hlx & Hownst & Hst)". revert Hm1.
       destruct (decide (Z_of_rwlock_st st = Z_of_rwlock_st st')) as [->|?]=>?.
       + iApply (wp_cas_int_suc with "Hlx"); first done. iNext. iIntros "Hlx".
@@ -215,26 +216,24 @@ Section rwlock_functions.
             iExists _. iFrame. iExists _, _. iSplitR; first done. iFrame "#∗".
             rewrite Qp_div_2. iSplitL; last done.
             iIntros "!> Hν". iApply "Hh". rewrite -lft_dead_or. auto. }
-        iMod ("Hclose'" with "[$INV]") as "Hβtok1".
+        iMod ("Hclose''" with "[$INV]") as "Hβtok1".
         iApply (wp_if _ true). iIntros "!>!>".
-        iMod ("Hclose" with "[$Hβtok1 $Hβtok2]") as "HE".
+        iMod ("Hclose'" with "[$]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
         iApply (type_type  _ _ _
                    [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2);
                      #lx ◁ rwlockreadguard α ty]%TC
-              with "[] LFT Hna [> HE] HL Hk"); first last.
+              with "[] LFT HE Hna HL Hk"); first last.
         { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
                   tctx_hasty_val' //. iFrame.
           iExists _, _, _, _. iFrame "∗#". iApply ty_shr_mono; last done.
           iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
-        { rewrite {1}/elctx_interp big_sepL_singleton //. }
         iApply (type_sum_assign (option $ rwlockreadguard α ty)); [solve_typing..|].
         simpl. iApply type_jump; solve_typing.
       + iApply (wp_cas_int_fail with "Hlx"); try done. iNext. iIntros "Hlx".
-        iMod ("Hclose'" with "[Hlx Hownst Hst]") as "Hβtok1"; first by iExists _; iFrame.
+        iMod ("Hclose''" with "[Hlx Hownst Hst]") as "Hβtok1"; first by iExists _; iFrame.
         iModIntro. iApply (wp_if _ false). iNext.
-        iMod ("Hclose" with "[$Hβtok1 $Hβtok2]") as "HE".
-        iSpecialize ("Hk" with "[HE] []").
-        { by rewrite {1}/elctx_interp big_sepL_singleton. } solve_typing.
+        iMod ("Hclose'" with "[$]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+        iSpecialize ("Hk" with "[]"); first solve_typing.
         iApply ("Hk" $! [#] with "Hna HL").
         rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
         iExists _. iSplit. done. simpl. eauto.
@@ -257,50 +256,50 @@ Section rwlock_functions.
 
   Lemma rwlock_try_write_type ty :
     typed_val rwlock_try_write
-        (fn(∀ α, [α]; &shr{α}(rwlock ty)) → option (rwlockwriteguard α ty)).
+        (fn(∀ α, λ ϝ, [ϝ ⊑ α]; &shr{α}(rwlock ty)) → option (rwlockwriteguard α ty)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
-    iApply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} rwlock ty);
-                                    r!!!0 ◁ box (option (rwlockwriteguard α ty))])%TC);
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply (type_cont [_] [ϝ ⊑ []]%LL (λ r, [x ◁ box (&shr{α} rwlock ty);
+                                        r!!!0 ◁ box (option (rwlockwriteguard α ty))])%TC);
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r];
       simpl_subst; last first.
     { 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 qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+    iIntros (x' tid) "#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]".
-    rewrite {1}/elctx_interp big_sepL_singleton.
-    iMod (lft_incl_acc with "Hαβ HE") as (qβ) "[Hβtok Hclose]". done.
+    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βtok Hclose']". done.
     wp_bind (CAS _ _ _).
-    iMod (shr_bor_acc_tok with "LFT Hinv Hβtok") as "(INV & Hclose')"; try done.
+    iMod (shr_bor_acc_tok with "LFT Hinv Hβtok") as "[INV Hclose'']"; try done.
     iDestruct "INV" as (st) "(Hlx & >Hownst & Hst)". destruct st.
     - iApply (wp_cas_int_fail with "Hlx"). done. by destruct c as [|[[]]|].
       iNext. iIntros "Hlx".
-      iMod ("Hclose'" with "[Hlx Hownst Hst]") as "Hβtok"; first by iExists _; iFrame.
+      iMod ("Hclose''" with "[Hlx Hownst Hst]") as "Hβtok"; first by iExists _; iFrame.
+      iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
       iModIntro. iApply (wp_if _ false). iNext.
       iApply (type_type _ _ _
               [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2) ]%TC
-              with "[] LFT Hna [> Hclose Hβtok] HL Hk"); first last.
+              with "[] LFT HE Hna HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
-      { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_unit (option $ rwlockwriteguard α ty));
         [solve_typing..|]; first last.
       rewrite /option /=. iApply type_jump; solve_typing.
     - iApply (wp_cas_int_suc with "Hlx"). done. iIntros "!> Hlx".
       iMod (own_update with "Hownst") as "[Hownst ?]".
       { by eapply auth_update_alloc, (op_local_update_discrete _ _ writing_st). }
-      iMod ("Hclose'" with "[Hlx Hownst]") as "Hβtok". { iExists _. iFrame. }
-      iModIntro. iApply (wp_if _ true). iNext. iMod ("Hclose" with "Hβtok") as "HE".
+      iMod ("Hclose''" with "[Hlx Hownst]") as "Hβtok". { iExists _. iFrame. }
+      iModIntro. iApply (wp_if _ true). iNext. iMod ("Hclose'" with "Hβtok") as "Hα".
+      iMod ("Hclose" with "Hα HL") as "HL".
       iApply (type_type  _ _ _
                    [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2);
                      #lx ◁ rwlockwriteguard α ty]%TC
-              with "[] LFT Hna [> HE] HL Hk"); first last.
+              with "[] LFT HE Hna HL Hk"); first last.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
                 tctx_hasty_val' //. iFrame.  iExists _, _. iFrame "∗#". }
-      { rewrite {1}/elctx_interp big_sepL_singleton //. }
       iApply (type_sum_assign (option $ rwlockwriteguard α ty)); [solve_typing..|].
       simpl. iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 6388002fa6c586dd4d1362ab65f707e6ac094855..e023b7a3515552e5c8c6da60486a167a2b07abbf 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -75,19 +75,21 @@ 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) "#HE #HL".
-    iDestruct (proj1 Hty with "HE HL") as "(%&#Ho&#Hs)".
-    iDestruct (Hα with "HE HL") as "Hα1α2".
-    iSplit; [|iSplit; iAlways].
+    iIntros (α1 α2 Hα ty1 ty2 Hty q) "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".
+    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iAlways].
     - done.
     - iIntros (tid [|[[]|][]]) "H"; try done.
-      iDestruct "H" as (ν q γ β) "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
-      iExists ν, q, γ, β. iFrame "∗#". iSplit; last iSplit.
+      iDestruct "H" as (ν q' γ β) "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
+      iExists ν, q', γ, β. 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 (shr_bor_iff with "[] Hinv").
-        iIntros "!> !#"; iSplit; iIntros "H"; by iApply rwlock_inv_proper.
+        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.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 08917456fbbd5185116ea1eb49b95748b0bd1332..4fb1418b380fcc6216ed3b6a2a1c6e16b6f4b70c 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -20,28 +20,26 @@ Section rwlockreadguard_functions.
 
   Lemma rwlockreadguard_deref_type ty :
     typed_val rwlockreadguard_deref
-      (fn (fun '(α, β) => FP [α; β; α ⊑ β]%EL
-                              [# &shr{α}(rwlockreadguard β ty)] (&shr{α}ty))).
+      (fn (fun '(α, β) => FP (λ ϝ, [ϝ ⊑ α; α ⊑ β]%EL)
+                             [# &shr{α}(rwlockreadguard β ty)] (&shr{α}ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
+      iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
-    iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
     iDestruct "Hx'" as (l') "#[Hfrac Hshr]".
-    rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
-    iDestruct "HE" as "(Hα & Hβ & #Hαβ)".
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
     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↦]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} rwlockreadguard β ty);
                               #(shift_loc l' 1) ◁ &shr{α}ty]%TC
-      with "[] LFT Hna [Hα Hβ Hαβ] HL Hk"); first last.
+      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. done.
-      iApply lft_incl_refl. }
-    { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
+      iFrame. iApply (ty_shr_mono with "[] Hshr"). iApply lft_incl_glb.
+      by iDestruct "HE" as "(_ & $ & _)". by iApply lft_incl_refl. }
     iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -62,22 +60,21 @@ Section rwlockreadguard_functions.
 
   Lemma rwlockreadguard_drop_type ty :
     typed_val rwlockreadguard_drop
-              (fn(∀ α, [α]; rwlockreadguard α ty) → unit).
+              (fn(∀ α, λ ϝ, [ϝ ⊑ α]; rwlockreadguard α ty) → unit).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_deref; [solve_typing..|].
-      iIntros (x'). simpl_subst.
-    iApply (type_cont [] [] (λ _, [x ◁ _; x' ◁ _])%TC);
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+    iApply (type_cont [] [ϝ ⊑ []]%LL (λ _, [x ◁ _; x' ◁ _])%TC);
       [iIntros (loop)|iIntros "/= !#"; iIntros (loop arg); inv_vec arg];
       simpl_subst.
     { iApply type_jump; solve_typing. }
-    iIntros (tid qE) "#LFT Hna Hα HL Hk HT".
-    rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_cons
-            tctx_interp_singleton !tctx_hasty_val.
+    iIntros (tid) "#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.
     iDestruct "Hx'" as (ν q γ β) "(Hx' & #Hαβ & #Hinv & Hν & H◯ & H†)".
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
     iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
     wp_bind (!ˢᶜ#lx')%E.
     iMod (shr_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
@@ -126,22 +123,22 @@ Section rwlockreadguard_functions.
       iApply (wp_step_fupd with "INV"). done. set_solver.
       iApply (wp_cas_int_suc with "Hlx"); try done. iNext. iIntros "Hlx INV !>".
       iMod ("INV" with "Hlx") as "INV". iMod ("Hcloseβ" with "[$INV]") as "Hβ".
-      iMod ("Hcloseα" with "Hβ") as "HE". iApply (wp_if _ true). iIntros "!>!>".
+      iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+      iApply (wp_if _ true). iIntros "!>!>".
       iApply (type_type _ _ _ [ x ◁ box (uninit 1)]%TC
-              with "[] LFT Hna [HE] HL Hk"); first last.
+              with "[] LFT HE Hna HL Hk"); first last.
       { rewrite tctx_interp_singleton tctx_hasty_val //. }
-      { rewrite /elctx_interp big_sepL_singleton //. }
       iApply type_delete; [solve_typing..|].
       iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
       iApply type_jump; solve_typing.
     + iApply (wp_cas_int_fail with "Hlx"); try done. iNext. iIntros "Hlx".
       iMod ("Hcloseβ" with "[Hlx H● Hst]") as "Hβ". by iExists _; iFrame.
-      iMod ("Hcloseα" with "Hβ") as "HE". iApply (wp_if _ false). iIntros "!> !>".
+      iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+      iApply (wp_if _ false). iIntros "!> !>".
       iApply (type_type _ _ _ [ x ◁ box (uninit 1); #lx' ◁ rwlockreadguard α ty]%TC
-              with "[] LFT Hna [HE] HL Hk"); first last.
+              with "[] LFT HE Hna HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val
-                tctx_hasty_val' //. iFrame. iExists _, _, _, _. iFrame "∗#". }
-      { rewrite /elctx_interp big_sepL_singleton //. }
+                tctx_hasty_val' //=. auto 10 with iFrame. }
       iApply type_jump; solve_typing.
   Qed.
 End rwlockreadguard_functions.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index ca13f922e59c1437c7ba83a0107e2f9aee1b82b1..b71f6c763fb6bb7a9f0683567dedfa4d4cf16af2 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -73,11 +73,12 @@ Section rwlockwriteguard.
   Global Instance rwlockwriteguard_mono E L :
     Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) rwlockwriteguard.
   Proof.
-    iIntros (α1 α2 Hα ty1 ty2 Hty) "#HE #HL".
-    pose proof Hty as Hty'%eqtype_unfold.
-    iDestruct (Hty' with "HE HL") as "(%&#Ho&#Hs)".
-    iDestruct (Hα with "HE HL") as "Hα1α2".
-    iSplit; [|iSplit; iAlways].
+    intros α1 α2 Hα ty1 ty2 Hty. generalize Hty. rewrite eqtype_unfold. iIntros (Hty' q) "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".
+    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iAlways].
     - done.
     - iIntros (tid [|[[]|][]]) "H"; try done.
       iDestruct "H" as (γ β) "(Hb & #H⊑ & #Hinv & Hown)".
@@ -87,7 +88,7 @@ Section rwlockwriteguard.
         iExists vl; iFrame; by iApply "Ho".
       + by iApply lft_incl_trans.
       + iApply shr_bor_iff; try done.
-        iIntros "!>!#"; iSplit; iIntros "H"; by iApply rwlock_inv_proper.
+        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]". set_solver.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index d46cf2071e319bcf75d814de68dd9b14e0d5d478..ba11a3a3b02cca2030029fd36efb7a52b304fa55 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -20,33 +20,35 @@ Section rwlockwriteguard_functions.
 
   Lemma rwlockwriteguard_deref_type ty :
     typed_val rwlockwriteguard_deref
-      (fn (fun '(α, β) => FP [α; β; α ⊑ β]%EL
-                              [# &shr{α}(rwlockwriteguard β ty)] (&shr{α}ty))).
+      (fn (fun '(α, β) => FP (λ ϝ, [ϝ ⊑ α; α ⊑ β]%EL)
+                             [# &shr{α}(rwlockwriteguard β ty)] (&shr{α}ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
+      iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
-    iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
     iDestruct "Hx'" as (l') "#[Hfrac Hshr]".
-    rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
-    iDestruct "HE" as "([Hα1 Hα2] & Hβ & #Hαβ)".
+    iMod (lctx_lft_alive_tok α 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.
     rewrite heap_mapsto_vec_singleton.
+    iMod (lctx_lft_alive_tok β 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β]");
          [done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
     iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β]!>". wp_op. wp_let.
     iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
-    iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1".
+    iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1". iMod ("Hclose'" with "Hβ HL") as "HL".
+    iMod ("Hclose" with "[$] HL") as "HL".
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} rwlockwriteguard β ty);
                               #(shift_loc l' 1) ◁ &shr{α}ty]%TC
-            with "[] LFT Hna [Hα1 Hα2 Hβ Hαβ] HL Hk"); last first.
+            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.
-      iApply lft_incl_refl. }
-    { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
+      iFrame. iApply (ty_shr_mono with "[] Hshr'"). iApply lft_incl_glb.
+        by iDestruct "HE" as "(_ & $ & _)". by iApply lft_incl_refl. }
     iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
     iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -62,19 +64,18 @@ Section rwlockwriteguard_functions.
 
   Lemma rwlockwriteguard_derefmut_type ty :
     typed_val rwlockwriteguard_derefmut
-      (fn (fun '(α, β) => FP [α; β; α ⊑ β]%EL
-                              [# &uniq{α}(rwlockwriteguard β ty)] (&uniq{α}ty))).
+      (fn (fun '(α, β) => FP (λ ϝ, [ϝ ⊑ α; α ⊑ β]%EL)
+                             [# &uniq{α}(rwlockwriteguard β ty)] (&uniq{α}ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
+      iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
-    iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-    iDestruct "HT" as "[Hx Hx']".
-    rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
-    iDestruct "HE" as "(Hα & Hβ & #Hαβ)". destruct x' as [[|lx'|]|]; try done.
+    iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
     iMod (bor_exists with "LFT Hx'") as (vl) "H". done.
     iMod (bor_sep with "LFT H") as "[H↦ H]". done.
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
     destruct vl as [|[[|l|]|][]];
       try by iMod (bor_persistent_tok with "LFT H Hα") as "[>[] _]".
     rewrite heap_mapsto_vec_singleton.
@@ -87,13 +88,13 @@ Section rwlockwriteguard_functions.
     wp_bind (!(LitV lx'))%E. iApply (wp_step_fupd with "[Hb]");
       [done| |by iApply (bor_unnest with "LFT Hb")|]; first done.
     wp_read. iIntros "Hb !>". wp_op. wp_let.
-    iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]".
+    iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]". iMod ("Hclose" with "Hα HL") as "HL".
     iApply (type_type _ _ _ [ x ◁ box (uninit 1); #(shift_loc l 1) ◁ &uniq{α}ty]%TC
-            with "[] LFT Hna [Hα Hβ Hαβ] HL Hk"); last first.
+            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_trans|iApply lft_incl_refl]. }
-    { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
+      iFrame. iApply (bor_shorten with "[] Hb"). iApply lft_incl_glb.
+      by iApply lft_incl_trans; first iDestruct "HE" as "(_ & $ & _)".
+      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.
@@ -109,17 +110,17 @@ Section rwlockwriteguard_functions.
 
   Lemma rwlockwriteguard_drop_type ty :
     typed_val rwlockwriteguard_drop
-              (fn(∀ α, [α]; rwlockwriteguard α ty) → unit).
+              (fn(∀ α, λ ϝ, [ϝ ⊑ α]; rwlockwriteguard α ty) → unit).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
-    iIntros (tid qE) "#LFT Hna Hα HL Hk HT".
-    rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_cons
-            tctx_interp_singleton !tctx_hasty_val.
+    iIntros (tid) "#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.
     iDestruct "Hx'" as (γ β) "(Hx' & #Hαβ & #Hinv & H◯)".
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
     iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
     wp_bind (#lx' <-ˢᶜ #0)%E.
     iMod (shr_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
@@ -132,11 +133,11 @@ Section rwlockwriteguard_functions.
       iExists None. iFrame. iMod (own_update_2 with "H● H◯") as "$"; last done.
       apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
       apply cancel_local_update_empty, _. }
-    iModIntro. wp_seq. iMod ("Hcloseα" with "Hβ") as "HE".
+    iModIntro. wp_seq. iMod ("Hcloseα" with "Hβ") as "Hα".
+    iMod ("Hclose" with "Hα HL") as "HL".
     iApply (type_type _ _ _ [ x ◁ box (uninit 1)]%TC
-            with "[] LFT Hna [HE] HL Hk"); first last.
+            with "[] LFT HE Hna HL Hk"); first last.
     { rewrite tctx_interp_singleton tctx_hasty_val //. }
-    { rewrite /elctx_interp big_sepL_singleton //. }
     iApply type_delete; [solve_typing..|].
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_jump; solve_typing.