diff --git a/theories/frac_borrow.v b/theories/frac_borrow.v
index fa85e2aa562f5c0e3a270cea2fa57e029dc6ba32..f68755d8bd070e3514cd8968297116dfc1d7c891 100644
--- a/theories/frac_borrow.v
+++ b/theories/frac_borrow.v
@@ -21,28 +21,28 @@ Section frac_borrow.
   Global Instance frac_borrow_persistent : PersistentP (&frac{κ}φ) := _.
 
   Lemma borrow_fracture φ `(nclose lftN ⊆ E) κ:
-    &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
+    lft_ctx ⊢ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
   Proof.
-    iIntros "Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
-    iMod (borrow_acc_atomic_strong with "Hφ") as "[[Hφ Hclose]|[H† Hclose]]". done.
+    iIntros "#LFT Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
+    iMod (borrow_acc_atomic_strong with "LFT Hφ") as "[[Hφ Hclose]|[H† Hclose]]". done.
     - iMod ("Hclose" with "*[-]") as "Hφ"; last first.
       { iExists γ, κ. iSplitR; last by iApply (borrow_share with "Hφ").
         iApply lft_incl_refl. }
       iSplitL. by iExists 1%Qp; iFrame; auto.
-      iIntros "!>[H† Hφ]!>". iNext. iDestruct "Hφ" as (q') "(Hφ & _ & [%|Hκ])". by subst.
+      iIntros "!>H† Hφ!>". iNext. iDestruct "Hφ" as (q') "(Hφ & _ & [%|Hκ])". by subst.
       iDestruct "Hκ" as (q'') "[_ Hκ]".
-      iDestruct (lft_own_dead with "[$Hκ $H†]") as "[]".
+      iDestruct (lft_own_dead with "Hκ H†") as "[]".
     - iMod ("Hclose" with "*") as "Hφ"; last first.
       iExists γ, κ. iSplitR. by iApply lft_incl_refl.
-      iMod (borrow_fake with "H†"). done. by iApply borrow_share.
+      iMod (borrow_fake with "LFT H†"). done. by iApply borrow_share.
   Qed.
 
   Lemma frac_borrow_atomic_acc `(nclose lftN ⊆ E) κ φ:
-    &frac{κ}φ ={E,E∖lftN}=∗ (∃ q, ▷ φ q ∗ (▷ φ q ={E∖lftN,E}=∗ True))
-                          ∨ [†κ] ∗ |={E∖lftN,E}=> True.
+    lft_ctx ⊢ &frac{κ}φ ={E,E∖lftN}=∗ (∃ q, ▷ φ q ∗ (▷ φ q ={E∖lftN,E}=∗ True))
+                                      ∨ [†κ] ∗ |={E∖lftN,E}=> True.
   Proof.
-    iIntros "#Hφ". iDestruct "Hφ" as (γ κ') "[Hκκ' Hshr]".
-    iMod (shr_borrow_acc with "Hshr") as "[[Hφ Hclose]|[H† Hclose]]". done.
+    iIntros "#LFT #Hφ". iDestruct "Hφ" as (γ κ') "[Hκκ' Hshr]".
+    iMod (shr_borrow_acc with "LFT Hshr") as "[[Hφ Hclose]|[H† Hclose]]". done.
     - iLeft. iDestruct "Hφ" as (q) "(Hφ & Hγ & H)". iExists q. iFrame.
       iIntros "!>Hφ". iApply "Hclose". iExists q. iFrame.
     - iRight. iMod "Hclose" as "_". iMod (lft_incl_dead with "Hκκ' H†") as "$". done.
@@ -50,13 +50,13 @@ Section frac_borrow.
   Qed.
 
   Lemma frac_borrow_acc `(nclose lftN ⊆ E) q κ φ:
-    □ (∀ q1 q2, φ (q1+q2)%Qp ↔ φ q1 ∗ φ q2) ⊢
+    lft_ctx ⊢ □ (∀ q1 q2, φ (q1+q2)%Qp ↔ φ q1 ∗ φ q2) -∗
     &frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={E}=∗ q.[κ]).
   Proof.
-    iIntros "#Hφ Hfrac Hκ". unfold frac_borrow.
+    iIntros "#LFT #Hφ Hfrac Hκ". unfold frac_borrow.
     iDestruct "Hfrac" as (γ κ') "#[#Hκκ' Hshr]".
     iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[[Hκ1 Hκ2] Hclose]". done.
-    iMod (shr_borrow_acc_tok with "Hshr Hκ1") as "[H Hclose']". done.
+    iMod (shr_borrow_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
     iDestruct "H" as (qφ) "(Hφqφ & >Hown & Hq)".
     destruct (Qp_lower_bound (qκ'/2) (qφ/2)) as (qq & qκ'0 & qφ0 & Hqκ' & Hqφ).
     iExists qq.
@@ -72,7 +72,7 @@ Section frac_borrow.
         rewrite lft_own_frac_op. iIntros "{$Hκq $Hq'κ}!%".
         by rewrite assoc (comm _ _ qq) assoc -Hqφ Qp_div_2. }
     clear Hqφ qφ qφ0. iIntros "!>Hqφ".
-    iMod (shr_borrow_acc_tok with "Hshr Hκ1") as "[H Hclose']". done.
+    iMod (shr_borrow_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
     iDestruct "H" as (qφ) "(Hφqφ & >Hown & >[%|Hq])".
     { subst. iCombine "Hown" "Hownq" as "Hown".
       by iDestruct (own_valid with "Hown") as %Hval%Qp_not_plus_q_ge_1. }
@@ -102,17 +102,17 @@ Section frac_borrow.
   Qed.
 
   Lemma frac_borrow_incl κ κ' q:
-    &frac{κ}(λ q', (q * q').[κ']) ⊢ κ ⊑ κ'.
+    lft_ctx ⊢ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
   Proof.
-    iIntros "#Hbor!#". iSplitR.
+    iIntros "#LFT#Hbor!#". iSplitR.
     - iIntros (q') "Hκ'".
-      iMod (frac_borrow_acc with "[] Hbor Hκ'") as (q'') "[>? Hclose]". done.
+      iMod (frac_borrow_acc with "LFT [] Hbor Hκ'") as (q'') "[>? Hclose]". done.
       + iIntros "/=!#*". rewrite Qp_mult_plus_distr_r lft_own_frac_op. iSplit; auto.
       + iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
     - iIntros "H†'".
-      iMod (frac_borrow_atomic_acc with "Hbor") as "[H|[$ $]]". done.
+      iMod (frac_borrow_atomic_acc with "LFT Hbor") as "[H|[$ $]]". done.
       iDestruct "H" as (q') "[>Hκ' _]".
-      iDestruct (lft_own_dead with "[$H†' $Hκ']") as "[]".
+      iDestruct (lft_own_dead with "Hκ' H†'") as "[]".
   Qed.
 
 End frac_borrow.
diff --git a/theories/lifetime.v b/theories/lifetime.v
index bfa9e8d9e4433c98ae8878bf5c70855980009aa6..4d705fdb6e1d6047c6a8ab98bd7b586f4297608d 100644
--- a/theories/lifetime.v
+++ b/theories/lifetime.v
@@ -21,6 +21,8 @@ Class lifetimeG Σ := LifetimeG {
   borrow_tok_name : gname
 }.
 
+Parameter lft_ctx : ∀ `{lifetimeG Σ}, iProp Σ.
+
 Section defs.
 
   (*** Definitions  *)
@@ -69,6 +71,8 @@ Hint Unfold lifetime : typeclass_instances.
 Section lft.
   Context `{invG Σ, lifetimeG Σ}.
 
+  Axiom lft_ctx_alloc : True ={∅}=∗ lft_ctx.
+
   (*** PersitentP, TimelessP and Proper instances  *)
 
   Global Instance lft_own_timeless q κ : TimelessP q.[κ].
@@ -93,6 +97,8 @@ Section lft.
   Global Instance borrow_proper κ: Proper ((⊣⊢) ==> (⊣⊢)) (borrow κ).
   Proof. solve_proper. Qed.
 
+  Axiom lft_ctx_persistent : PersistentP lft_ctx.
+
   (** Basic rules about lifetimes  *)
   Lemma lft_own_op q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⋅ κ2].
   Proof.
@@ -127,48 +133,49 @@ Section lft.
   Qed.
 
   Axiom lft_create :
-    ∀ `(nclose lftN ⊆ E), True ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,⊤∖nclose lftN}▷=∗ [†κ]).
+    ∀ `(nclose lftN ⊆ E),
+      lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,⊤∖nclose lftN}▷=∗ [†κ]).
 
   Axiom idx_borrow_acc :
     ∀ `(nclose lftN ⊆ E) q κ i P,
-      idx_borrow κ i P ⊢ idx_borrow_own 1 i ∗ q.[κ] ={E}=∗ ▷ P ∗
-                                 (▷ P ={E}=∗ idx_borrow_own 1 i ∗ q.[κ]).
+      lft_ctx ⊢ idx_borrow κ i P -∗ idx_borrow_own 1 i
+              -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ idx_borrow_own 1 i ∗ q.[κ]).
   Axiom idx_borrow_atomic_acc :
     ∀ `(nclose lftN ⊆ E) q κ i P,
-      idx_borrow κ i P ⊢ idx_borrow_own q i
+      lft_ctx ⊢ idx_borrow κ i P -∗ idx_borrow_own q i
          ={E,E∖lftN}=∗
             ▷ P ∗ (▷ P ={E∖lftN,E}=∗ idx_borrow_own q i) ∨
             [†κ] ∗ (|={E∖lftN,E}=> idx_borrow_own q i).
 
   (** Basic borrows  *)
   Axiom borrow_create :
-    ∀ `(nclose lftN ⊆ E) κ P, ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
-  Axiom borrow_fake : ∀ `(nclose lftN ⊆ E) κ P, [†κ] ={E}=∗ &{κ}P.
+    ∀ `(nclose lftN ⊆ E) κ P, lft_ctx ⊢ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
+  Axiom borrow_fake : ∀ `(nclose lftN ⊆ E) κ P, lft_ctx ⊢ [†κ] ={E}=∗ &{κ}P.
   Axiom borrow_split :
-    ∀ `(nclose lftN ⊆ E) κ P Q, &{κ}(P ∗ Q) ={E}=∗ &{κ}P ∗ &{κ}Q.
+    ∀ `(nclose lftN ⊆ E) κ P Q, lft_ctx ⊢ &{κ}(P ∗ Q) ={E}=∗ &{κ}P ∗ &{κ}Q.
   Axiom borrow_combine :
-    ∀ `(nclose lftN ⊆ E) κ P Q, &{κ}P ∗ &{κ}Q ={E}=∗ &{κ}(P ∗ Q).
+    ∀ `(nclose lftN ⊆ E) κ P Q, lft_ctx ⊢ &{κ}P -∗ &{κ}Q ={E}=∗ &{κ}(P ∗ Q).
   Axiom borrow_acc_strong :
     ∀ `(nclose lftN ⊆ E) q κ P,
-      &{κ}P ⊢ q.[κ] ={E}=∗ ▷ P ∗
-      ∀ Q, ▷ Q ∗ ▷([†κ] ∗ ▷Q ={⊤ ∖ nclose lftN}=∗ ▷ P) ={E}=∗ &{κ}Q ∗ q.[κ].
+      lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗
+      ∀ Q, ▷ Q ∗ ▷([†κ] -∗ ▷Q ={⊤ ∖ nclose lftN}=∗ ▷ P) ={E}=∗ &{κ}Q ∗ q.[κ].
   Axiom borrow_acc_atomic_strong :
     ∀ `(nclose lftN ⊆ E) κ P,
-      &{κ}P ={E,E∖lftN}=∗
-        (▷ P ∗ ∀ Q, ▷ Q ∗ ▷([†κ] ∗ ▷Q ={⊤ ∖ nclose lftN}=∗ ▷ P) ={E∖lftN,E}=∗ &{κ}Q) ∨
+      lft_ctx ⊢ &{κ}P ={E,E∖lftN}=∗
+        (▷ P ∗ ∀ Q, ▷ Q ∗ ▷([†κ] -∗ ▷Q ={⊤ ∖ nclose lftN}=∗ ▷ P) ={E∖lftN,E}=∗ &{κ}Q) ∨
         [†κ] ∗ |={E∖lftN,E}=> True.
   Axiom borrow_reborrow' :
     ∀ `(nclose lftN ⊆ E) κ κ' P, κ ≼ κ' →
-      &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
+      lft_ctx ⊢ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
   Axiom borrow_unnest :
-    ∀ `(nclose lftN ⊆ E) κ κ' P, &{κ'}&{κ}P ⊢ |={E}▷=> &{κ ⋅ κ'}P.
+    ∀ `(nclose lftN ⊆ E) κ κ' P, lft_ctx ⊢ &{κ'}&{κ}P ={E}▷=∗ &{κ ⋅ κ'}P.
 
   (*** Derived lemmas  *)
 
-  Lemma lft_own_dead q κ : q.[κ] ∗ [† κ] ⊢ False.
+  Lemma lft_own_dead q κ : q.[κ] ⊢ [† κ] -∗ False.
   Proof.
     rewrite /lft_own /lft_dead.
-    iIntros "[Hl Hr]". iDestruct "Hr" as (Λ) "[HΛ Hr]".
+    iIntros "Hl Hr". iDestruct "Hr" as (Λ) "[HΛ Hr]".
     iDestruct "HΛ" as %[n HΛ].
     iDestruct (own_valid_2 with "[$Hl $Hr]") as %Hval. iPureIntro.
     generalize (Hval Λ).
@@ -219,33 +226,34 @@ Section lft.
   Proof. by rewrite /FromSep lft_own_op. Qed.
 
   Lemma borrow_acc E q κ P : nclose lftN ⊆ E →
-      &{κ}P ⊢ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
+      lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
   Proof.
-    iIntros (?) "HP Htok".
-    iMod (borrow_acc_strong with "HP Htok") as "[HP Hclose]". done.
-    iIntros "!> {$HP} HP". iApply "Hclose". by iIntros "{$HP}!>[_$]".
+    iIntros (?) "#LFT HP Htok".
+    iMod (borrow_acc_strong with "LFT HP Htok") as "[HP Hclose]". done.
+    iIntros "!> {$HP} HP". iApply "Hclose". by iIntros "{$HP}!>_$".
   Qed.
 
   Lemma borrow_exists {A} `(nclose lftN ⊆ E) κ (Φ : A → iProp Σ) {_:Inhabited A}:
-    &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
+    lft_ctx ⊢ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
   Proof.
-    iIntros "Hb". iMod (borrow_acc_atomic_strong with "Hb") as "[[HΦ Hclose]|[H† Hclose]]". done.
-    - iDestruct "HΦ" as (x) "HΦ". iExists x. iApply "Hclose". iIntros "{$HΦ}!>[_?]". eauto.
-    - iMod "Hclose" as "_". iExists inhabitant. by iApply borrow_fake.
+    iIntros "#LFT Hb".
+    iMod (borrow_acc_atomic_strong with "LFT Hb") as "[[HΦ Hclose]|[H† Hclose]]". done.
+    - iDestruct "HΦ" as (x) "HΦ". iExists x. iApply "Hclose". iIntros "{$HΦ}!>_?". eauto.
+    - iMod "Hclose" as "_". iExists inhabitant. by iApply (borrow_fake with "LFT").
   Qed.
 
   Lemma borrow_or `(nclose lftN ⊆ E) κ P Q:
-    &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
+    lft_ctx ⊢ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
   Proof.
-    iIntros "H". rewrite uPred.or_alt.
-    iMod (borrow_exists with "H") as ([]) "H"; auto.
+    iIntros "#LFT H". rewrite uPred.or_alt.
+    iMod (borrow_exists with "LFT H") as ([]) "H"; auto.
   Qed.
 
   Lemma borrow_persistent `(nclose lftN ⊆ E) `{PersistentP _ P} κ q:
-    &{κ}P ⊢ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
+    lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
   Proof.
-    iIntros "Hb Htok".
-    iMod (borrow_acc with "Hb Htok") as "[#HP Hob]". done.
+    iIntros "#LFT Hb Htok".
+    iMod (borrow_acc with "LFT Hb Htok") as "[#HP Hob]". done.
     by iMod ("Hob" with "HP") as "[_$]".
   Qed.
 
@@ -332,9 +340,9 @@ Section incl.
   Qed.
 
   Lemma reborrow `(nclose lftN ⊆ E) P κ κ':
-    κ' ⊑ κ ⊢ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗  &{κ}P).
+    lft_ctx ⊢ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗  &{κ}P).
   Proof.
-    iIntros "#H⊑ HP". iMod (borrow_reborrow' with "HP") as "[Hκ' H∋]".
+    iIntros "#LFT #H⊑ HP". iMod (borrow_reborrow' with "LFT HP") as "[Hκ' H∋]".
       done. by exists κ'.
     iDestruct (borrow_shorten with "[H⊑] Hκ'") as "$".
     { iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
diff --git a/theories/perm_incl.v b/theories/perm_incl.v
index d236d6bde8ea484ad879cd4ce0c1e90222806efc..4d646f391561e4efcc01630bd7c6b9de769e1b76 100644
--- a/theories/perm_incl.v
+++ b/theories/perm_incl.v
@@ -10,13 +10,13 @@ Section defs.
 
   (* Definitions *)
   Definition perm_incl (ρ1 ρ2 : perm) :=
-    ∀ tid, ρ1 tid ={⊤}=∗ ρ2 tid.
+    ∀ tid, lft_ctx ⊢ ρ1 tid ={⊤}=∗ ρ2 tid.
 
   Global Instance perm_equiv : Equiv perm :=
     λ ρ1 ρ2, perm_incl ρ1 ρ2 ∧ perm_incl ρ2 ρ1.
 
   Definition borrowing κ (ρ ρ1 ρ2 : perm) :=
-    ∀ tid, ρ tid ⊢ ρ1 tid ={⊤}=∗ ρ2 tid ∗ (κ ∋ ρ1)%P tid.
+    ∀ tid, lft_ctx ⊢ ρ tid -∗ ρ1 tid ={⊤}=∗ ρ2 tid ∗ (κ ∋ ρ1)%P tid.
 
 End defs.
 
@@ -36,7 +36,8 @@ Section props.
   Proof.
     split.
     - iIntros (? tid) "H". eauto.
-    - iIntros (??? H12 H23 tid) "H". iMod (H12 with "H") as "H". by iApply H23.
+    - iIntros (??? H12 H23 tid) "#LFT H".
+      iMod (H12 with "LFT H") as "H". by iApply (H23 with "LFT").
   Qed.
 
   Global Instance perm_equiv_equiv : Equivalence (⇔).
@@ -54,9 +55,9 @@ Section props.
   Global Instance perm_sep_proper :
     Proper ((⇔) ==> (⇔) ==> (⇔)) (sep).
   Proof.
-    intros ??[A B]??[C D]; split; iIntros (tid) "[A B]".
-    iMod (A with "A") as "$". iApply (C with "B").
-    iMod (B with "A") as "$". iApply (D with "B").
+    intros ??[A B]??[C D]; split; iIntros (tid) "#LFT [A B]".
+    iMod (A with "LFT A") as "$". iApply (C with "LFT B").
+    iMod (B with "LFT A") as "$". iApply (D with "LFT B").
   Qed.
 
   Lemma uPred_equiv_perm_equiv ρ θ : (∀ tid, ρ tid ⊣⊢ θ tid) → (ρ ⇔ θ).
@@ -66,49 +67,49 @@ Section props.
   Proof. iIntros (tid) "H". eauto. Qed.
 
   Lemma perm_incl_frame_l ρ ρ1 ρ2 : ρ1 ⇒ ρ2 → ρ ∗ ρ1 ⇒ ρ ∗ ρ2.
-  Proof. iIntros (Hρ tid) "[$?]". by iApply Hρ. Qed.
+  Proof. iIntros (Hρ tid) "#LFT [$?]". by iApply (Hρ with "LFT"). Qed.
 
   Lemma perm_incl_frame_r ρ ρ1 ρ2 :
     ρ1 ⇒ ρ2 → ρ1 ∗ ρ ⇒ ρ2 ∗ ρ.
-  Proof. iIntros (Hρ tid) "[?$]". by iApply Hρ. Qed.
+  Proof. iIntros (Hρ tid) "#LFT [?$]". by iApply (Hρ with "LFT"). Qed.
 
   Lemma perm_incl_exists_intro {A} P x : P x ⇒ ∃ x : A, P x.
-  Proof. iIntros (tid) "H!>". by iExists x. Qed.
+  Proof. iIntros (tid) "_ H!>". by iExists x. Qed.
 
   Global Instance perm_sep_assoc : Assoc (⇔) sep.
-  Proof. intros ???; split. by iIntros (tid) "[$[$$]]". by iIntros (tid) "[[$$]$]". Qed.
+  Proof. intros ???; split. by iIntros (tid) "_ [$[$$]]". by iIntros (tid) "_ [[$$]$]". Qed.
 
   Global Instance perm_sep_comm : Comm (⇔) sep.
-  Proof. intros ??; split; by iIntros (tid) "[$$]". Qed.
+  Proof. intros ??; split; by iIntros (tid) "_ [$$]". Qed.
 
   Global Instance perm_top_right_id : RightId (⇔) ⊤ sep.
-  Proof. intros ρ; split. by iIntros (tid) "[? _]". by iIntros (tid) "$". Qed.
+  Proof. intros ρ; split. by iIntros (tid) "_ [? _]". by iIntros (tid) "_ $". Qed.
 
   Global Instance perm_top_left_id : LeftId (⇔) ⊤ sep.
   Proof. intros ρ. by rewrite comm right_id. Qed.
 
   Lemma perm_incl_duplicable ρ (_ : Duplicable ρ) : ρ ⇒ ρ ∗ ρ.
-  Proof. iIntros (tid) "#H!>". by iSplit. Qed.
+  Proof. iIntros (tid) "_ #H!>". by iSplit. Qed.
 
   Lemma perm_tok_plus κ q1 q2 :
     tok κ q1 ∗ tok κ q2 ⇔ tok κ (q1 + q2).
   Proof.
-    rewrite /tok /sep /=; split; iIntros (tid) "?"; rewrite lft_own_frac_op //.
+    rewrite /tok /sep /=; split; iIntros (tid) "_ ?"; rewrite lft_own_frac_op //.
   Qed.
 
   Lemma perm_lftincl_refl κ : ⊤ ⇒ κ ⊑ κ.
-  Proof. iIntros (tid) "_!>". iApply lft_incl_refl. Qed.
+  Proof. iIntros (tid) "_ _!>". iApply lft_incl_refl. Qed.
 
   Lemma perm_lftincl_trans κ1 κ2 κ3 : κ1 ⊑ κ2 ∗ κ2 ⊑ κ3 ⇒ κ1 ⊑ κ3.
-  Proof. iIntros (tid) "[#?#?]!>". iApply lft_incl_trans. auto. Qed.
+  Proof. iIntros (tid) "_ [#?#?]!>". iApply lft_incl_trans. auto. Qed.
 
   Lemma perm_incl_share q ν κ ty :
     ν ◁ &uniq{κ} ty ∗ q.[κ] ⇒ ν ◁ &shr{κ} ty ∗ q.[κ].
   Proof.
-    iIntros (tid) "[Huniq [Htok $]]". unfold has_type.
+    iIntros (tid) "#LFT [Huniq [Htok $]]". unfold has_type.
     destruct (eval_expr ν); last by iDestruct "Huniq" as "[]".
     iDestruct "Huniq" as (l) "[% Hown]".
-    iMod (ty.(ty_share) _ lrustN with "Hown Htok") as "[Hown $]".
+    iMod (ty.(ty_share) _ lrustN with "LFT Hown Htok") as "[Hown $]".
     apply disjoint_union_l; solve_ndisj. done. iIntros "!>/=". eauto.
   Qed.
 
@@ -117,7 +118,7 @@ Section props.
       ν ◁ own q1 ty1 ∗ ν +ₗ #ty1.(ty_size) ◁ own q2 ty2.
   Proof.
     rewrite /has_type /own /sep /=.
-    destruct (eval_expr ν) as [[[]|?]|]; last first; split; iIntros (tid) "H/=";
+    destruct (eval_expr ν) as [[[]|?]|]; last first; split; iIntros (tid) "_ H/=";
       (try by iDestruct "H" as "[_ []]"); (try by iDestruct "H" as (l) "[% _]").
     { by auto. }
     - iDestruct "H" as (l') "(EQ & H & H†)". iDestruct "EQ" as %[=<-].
@@ -159,7 +160,7 @@ Section props.
     - destruct tyl as [|ty0 [|ty1 tyl]]; try done. simpl in *.
       assert (q0 = q) as ->. { apply Qp_eq. by rewrite -Hq Qcplus_0_r. }
       rewrite /has_type /sep /=.
-      destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "H/=";
+      destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "_ H/=";
         (try by iDestruct "H" as "[[] _]"); (try by iDestruct "H" as (l) "[% _]");
         (try by auto); rewrite (shift_loc_0 l) Nat.add_0_r.
       + iSplitL; last done. iExists _. iSplitR. done.
@@ -179,14 +180,14 @@ Section props.
       injection Hlen; intro Hlen'. rewrite perm_split_own_prod2 IH //.
       apply perm_sep_proper.
       + rewrite /has_type /sep /=.
-        destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "H/=";
+        destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "_ H/=";
         (try by iDestruct "H" as "[]"); (try by iDestruct "H" as (l) "[% _]");
         (try by auto); by rewrite shift_loc_0.
       + cut (length tyl = length (q1 :: ql)); last done. clear. revert tyl.
         generalize 0%nat. induction (q1 :: ql)=>offs -[|ty tyl] Hlen //.
         apply perm_sep_proper.
         * rewrite /has_type /sep /=.
-          destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "H/=";
+          destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "_ H/=";
           (try by iDestruct "H" as "[]"); (try by iDestruct "H" as (l) "[% _]");
           (try by auto); by rewrite shift_loc_assoc_nat (comm plus).
         * etransitivity. apply IHl. by injection Hlen. do 3 f_equiv. lia.
@@ -198,9 +199,9 @@ Section props.
   Proof.
     rewrite /has_type /sep /product2 /=.
     destruct (eval_expr ν) as [[[|l|]|]|];
-      iIntros (tid) "H"; try iDestruct "H" as "[]";
+      iIntros (tid) "#LFT H"; try iDestruct "H" as "[]";
         iDestruct "H" as (l0) "[EQ H]"; iDestruct "EQ" as %[=<-].
-    rewrite /= split_prod_mt. iMod (borrow_split with "H") as "[H1 H2]".
+    rewrite /= split_prod_mt. iMod (borrow_split with "LFT H") as "[H1 H2]".
     set_solver. iSplitL "H1"; eauto.
   Qed.
 
@@ -211,12 +212,12 @@ Section props.
             ⊤ (combine_offs tyl 0).
   Proof.
     transitivity (ν +ₗ #0%nat ◁ &uniq{κ}Π tyl)%P.
-    { iIntros (tid) "H/=". rewrite /has_type /=. destruct (eval_expr ν)=>//.
+    { iIntros (tid) "_ H/=". rewrite /has_type /=. destruct (eval_expr ν)=>//.
       iDestruct "H" as (l) "[Heq H]". iDestruct "Heq" as %[=->].
       rewrite shift_loc_0 /=. eauto. }
-    generalize 0%nat. induction tyl as [|ty tyl IH]=>offs. by iIntros (tid) "H/=".
+    generalize 0%nat. induction tyl as [|ty tyl IH]=>offs. by iIntros (tid) "_ H/=".
     etransitivity. apply perm_split_uniq_borrow_prod2.
-    iIntros (tid) "/=[$ H]". iApply IH. rewrite /has_type /=.
+    iIntros (tid) "#LFT /=[$ H]". iApply (IH with "LFT"). rewrite /has_type /=.
     destruct (eval_expr ν) as [[[]|]|]=>//=. by rewrite shift_loc_assoc_nat.
   Qed.
 
@@ -226,10 +227,10 @@ Section props.
   Proof.
     rewrite /has_type /sep /product2 /=.
     destruct (eval_expr ν) as [[[|l|]|]|];
-      iIntros (tid) "H"; try iDestruct "H" as "[]";
+      iIntros (tid) "#LFT H"; try iDestruct "H" as "[]";
         iDestruct "H" as (l0) "(EQ & H)"; iDestruct "EQ" as %[=<-].
     iDestruct "H" as (E1 E2) "(% & H1 & H2)".
-    iSplitL "H1"; iExists _; (iSplitR; [done|]); iApply (ty_shr_mono with "[]");
+    iSplitL "H1"; iExists _; (iSplitR; [done|]); iApply (ty_shr_mono with "LFT []");
       try by iFrame.
     set_solver. iApply lft_incl_refl. set_solver. iApply lft_incl_refl.
   Qed.
@@ -241,43 +242,43 @@ Section props.
             ⊤ (combine_offs tyl 0).
   Proof.
     transitivity (ν +ₗ #0%nat ◁ &shr{κ}Π tyl)%P.
-    { iIntros (tid) "H/=". rewrite /has_type /=. destruct (eval_expr ν)=>//.
+    { iIntros (tid) "#LFT H/=". rewrite /has_type /=. destruct (eval_expr ν)=>//.
       iDestruct "H" as (l) "[Heq H]". iDestruct "Heq" as %[=->].
       rewrite shift_loc_0 /=. iExists _. by iFrame "∗%". }
-    generalize 0%nat. induction tyl as [|ty tyl IH]=>offs. by iIntros (tid) "H/=".
+    generalize 0%nat. induction tyl as [|ty tyl IH]=>offs. by iIntros (tid) "_ H/=".
     etransitivity. apply perm_split_shr_borrow_prod2.
-    iIntros (tid) "/=[$ H]". iApply IH. rewrite /has_type /=.
+    iIntros (tid) "#LFT /=[$ H]". iApply (IH with "LFT"). rewrite /has_type /=.
     destruct (eval_expr ν) as [[[]|]|]=>//=. by rewrite shift_loc_assoc_nat.
   Qed.
 
   Lemma reborrow_shr_perm_incl κ κ' ν ty :
     κ ⊑ κ' ∗ ν ◁ &shr{κ'}ty ⇒ ν ◁ &shr{κ}ty.
   Proof.
-    iIntros (tid) "[#Hord #Hκ']". unfold has_type.
+    iIntros (tid) "#LFT [#Hord #Hκ']". unfold has_type.
     destruct (eval_expr ν) as [[[|l|]|]|];
       try by (iDestruct "Hκ'" as "[]" || iDestruct "Hκ'" as (l) "[% _]").
     iDestruct "Hκ'" as (l') "[EQ Hκ']". iDestruct "EQ" as %[=]. subst l'.
-    iModIntro. iExists _. iSplit. done. by iApply (ty_shr_mono with "Hord Hκ'").
+    iModIntro. iExists _. iSplit. done. by iApply (ty_shr_mono with "LFT Hord Hκ'").
   Qed.
 
   Lemma borrowing_perm_incl κ ρ ρ1 ρ2 θ :
     borrowing κ ρ ρ1 ρ2 → ρ ∗ κ ∋ θ ∗ ρ1 ⇒ ρ2 ∗ κ ∋ (θ ∗ ρ1).
   Proof.
-    iIntros (Hbor tid) "(Hρ&Hθ&Hρ1)". iMod (Hbor with "Hρ Hρ1") as "[$ Hρ1]".
+    iIntros (Hbor tid) "LFT (Hρ&Hθ&Hρ1)". iMod (Hbor with "LFT Hρ Hρ1") as "[$ Hρ1]".
     iIntros "!>#H†". iSplitL "Hθ". by iApply "Hθ". by iApply "Hρ1".
   Qed.
 
   Lemma own_uniq_borrowing ν q ty κ :
     borrowing κ ⊤ (ν ◁ own q ty) (ν ◁ &uniq{κ} ty).
   Proof.
-    iIntros (tid) "_ Hown". unfold has_type.
+    iIntros (tid) "#LFT _ Hown". unfold has_type.
     destruct (eval_expr ν) as [[[|l|]|]|];
       try by (iDestruct "Hown" as "[]" || iDestruct "Hown" as (l) "[% _]").
     iDestruct "Hown" as (l') "[EQ [Hown Hf]]". iDestruct "EQ" as %[=]. subst l'.
     iApply (fupd_mask_mono lftN). done.
-    iMod (borrow_create with "Hown") as "[Hbor Hext]". done.
+    iMod (borrow_create with "LFT Hown") as "[Hbor Hext]". done.
     iSplitL "Hbor". by simpl; eauto.
-    iMod (borrow_create with "Hf") as "[_ Hf]". done.
+    iMod (borrow_create with "LFT Hf") as "[_ Hf]". done.
     iIntros "!>#H†".
     iMod ("Hext" with "H†") as "Hext". iMod ("Hf" with "H†") as "Hf". iIntros "!>/=".
     iExists _. iFrame. auto.
@@ -286,23 +287,23 @@ Section props.
   Lemma reborrow_uniq_borrowing κ κ' ν ty :
     borrowing κ (κ ⊑ κ') (ν ◁ &uniq{κ'}ty) (ν ◁ &uniq{κ}ty).
   Proof.
-    iIntros (tid) "#Hord H". unfold has_type.
+    iIntros (tid) "#LFT #Hord H". unfold has_type.
     destruct (eval_expr ν) as [[[|l|]|]|];
       try by (iDestruct "H" as "[]" || iDestruct "H" as (l) "[% _]").
     iDestruct "H" as (l') "[EQ H]". iDestruct "EQ" as %[=]. subst l'.
     iApply (fupd_mask_mono lftN). done.
-    iMod (reborrow with "Hord H") as "[H Hextr]". done.
+    iMod (reborrow with "LFT Hord H") as "[H Hextr]". done.
     iModIntro. iSplitL "H". iExists _. by eauto.
     iIntros "H†". iMod ("Hextr" with "H†"). simpl. auto.
   Qed.
 
   Lemma lftincl_borrowing κ κ' q : borrowing κ ⊤ q.[κ'] (κ ⊑ κ').
   Proof.
-    iIntros (tid) "_ Htok". iApply fupd_mask_mono. done.
-    iMod (borrow_create with "[$Htok]") as "[Hbor Hclose]". reflexivity.
-    iMod (borrow_fracture (λ q', (q * q').[κ'])%I with "[Hbor]") as "Hbor". done.
+    iIntros (tid) "#LFT _ Htok". iApply fupd_mask_mono. done.
+    iMod (borrow_create with "LFT [$Htok]") as "[Hbor Hclose]". reflexivity.
+    iMod (borrow_fracture (λ q', (q * q').[κ'])%I with "LFT [Hbor]") as "Hbor". done.
     { by rewrite Qp_mult_1_r. }
-    iSplitL "Hbor". iApply frac_borrow_incl. done.
+    iSplitL "Hbor". iApply (frac_borrow_incl with "LFT Hbor").
     iIntros "!>H". by iMod ("Hclose" with "H") as ">$".
   Qed.
 
diff --git a/theories/shr_borrow.v b/theories/shr_borrow.v
index b586f64c693467f4f29cfcfb4cb3029263220a90..65714ea6a06397e9faf6d4776af86ed8627f722f 100644
--- a/theories/shr_borrow.v
+++ b/theories/shr_borrow.v
@@ -23,24 +23,25 @@ Section shared_borrows.
   Qed.
 
   Lemma shr_borrow_acc `(nclose lftN ⊆ E) κ :
-    &shr{κ}P ={E,E∖lftN}=∗ ▷P ∗ (▷P ={E∖lftN,E}=∗ True) ∨
+    lft_ctx ⊢ &shr{κ}P ={E,E∖lftN}=∗ ▷P ∗ (▷P ={E∖lftN,E}=∗ True) ∨
                           [†κ] ∗ |={E∖lftN,E}=> True.
   Proof.
-    iIntros "#HP". iDestruct "HP" as (i) "(#Hidx&#Hinv)".
+    iIntros "#LFT #HP". iDestruct "HP" as (i) "(#Hidx&#Hinv)".
     iInv lftN as (q') ">Hq'" "Hclose".
     rewrite -(Qp_div_2 q') /idx_borrow_own -op_singleton auth_frag_op own_op.
     iDestruct "Hq'" as "[Hq'0 Hq'1]". iMod ("Hclose" with "[Hq'1]") as "_". by eauto.
-    iMod (idx_borrow_atomic_acc with "Hidx Hq'0") as "[[HP Hclose]|[H† Hclose]]". done.
+    iMod (idx_borrow_atomic_acc with "LFT Hidx Hq'0") as "[[HP Hclose]|[H† Hclose]]". done.
     - iLeft. iFrame. iIntros "!>HP". by iMod ("Hclose" with "HP").
     - iRight. iFrame. iIntros "!>". by iMod "Hclose".
   Qed.
 
   Lemma shr_borrow_acc_tok `(nclose lftN ⊆ E) q κ :
-    &shr{κ}P ⊢ q.[κ] ={E,E∖lftN}=∗ ▷P ∗ (▷P ={E∖lftN,E}=∗ q.[κ]).
+    lft_ctx ⊢ &shr{κ}P -∗ q.[κ] ={E,E∖lftN}=∗ ▷P ∗ (▷P ={E∖lftN,E}=∗ q.[κ]).
   Proof.
-    iIntros "#Hshr Hκ". iMod (shr_borrow_acc with "Hshr") as "[[$ Hclose]|[H† _]]". done.
+    iIntros "#LFT #Hshr Hκ".
+    iMod (shr_borrow_acc with "LFT Hshr") as "[[$ Hclose]|[H† _]]". done.
     - iIntros "!>HP". by iMod ("Hclose" with "HP").
-    - iDestruct (lft_own_dead with "[-]") as "[]". by iFrame.
+    - iDestruct (lft_own_dead with "Hκ H†") as "[]".
   Qed.
 
   Lemma shr_borrow_shorten κ κ': κ ⊑ κ' ⊢ &shr{κ'}P -∗ &shr{κ}P.
diff --git a/theories/tl_borrow.v b/theories/tl_borrow.v
index 41bfa9b520eca978621e2925e98466d018eb98b3..b85f4058125674ef1c1f310483c8cc9bfab62953 100644
--- a/theories/tl_borrow.v
+++ b/theories/tl_borrow.v
@@ -28,14 +28,15 @@ Section tl_borrow.
 
   Lemma tl_borrow_acc q κ E F :
     nclose lftN ⊆ E → nclose tlN ⊆ E → nclose N ⊆ F →
-    &tl{κ|tid|N}P ⊢ q.[κ] ∗ tl_own tid F ={E}=∗ ▷P ∗ tl_own tid (F ∖ N) ∗
-                     (▷P ∗ tl_own tid (F ∖ N) ={E}=∗ q.[κ] ∗ tl_own tid F).
+    lft_ctx ⊢ &tl{κ|tid|N}P -∗ q.[κ] -∗ tl_own tid F ={E}=∗
+            ▷P ∗ tl_own tid (F ∖ N) ∗
+            (▷P -∗ tl_own tid (F ∖ N) ={E}=∗ q.[κ] ∗ tl_own tid F).
   Proof.
-    iIntros (???) "#HP[Hκ Htlown]".
+    iIntros (???) "#LFT#HP Hκ Htlown".
     iDestruct "HP" as (i) "(#Hpers&#Hinv)".
     iMod (tl_inv_open with "Hinv Htlown") as "(>Hown&Htlown&Hclose)"; try done.
-    iMod (idx_borrow_acc with "Hpers [$Hown $Hκ]") as "[HP Hclose']". done.
-    iIntros "{$HP $Htlown}!>[HP Htlown]".
+    iMod (idx_borrow_acc with "LFT Hpers Hown Hκ") as "[HP Hclose']". done.
+    iIntros "{$HP $Htlown}!>HP Htlown".
     iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
   Qed.
 
diff --git a/theories/type.v b/theories/type.v
index ab5148463c1af56f9f018354c13203992667f446..348046e5ba3d7e184829a226537b97963c0f51cd 100644
--- a/theories/type.v
+++ b/theories/type.v
@@ -40,12 +40,12 @@ Record type :=
        more consistent with thread-local tokens, which we do not
        give any. *)
     ty_share E N κ l tid q : mgmtE ⊥ nclose N → mgmtE ⊆ E →
-      &{κ} (l ↦∗: ty_own tid) ⊢ q.[κ] ={E}=∗ ty_shr κ tid N l ∗ q.[κ];
+      lft_ctx ⊢ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗ ty_shr κ tid N l ∗ q.[κ];
     ty_shr_mono κ κ' tid E E' l : E ⊆ E' →
-      κ' ⊑ κ ⊢ ty_shr κ tid E l -∗ ty_shr κ' tid E' l;
+      lft_ctx ⊢ κ' ⊑ κ -∗ ty_shr κ tid E l -∗ ty_shr κ' tid E' l;
     ty_shr_acc κ tid E F l q :
       ty_dup → mgmtE ∪ F ⊆ E →
-      ty_shr κ tid F l ⊢
+      lft_ctx ⊢ ty_shr κ tid F l -∗
         q.[κ] ∗ tl_own tid F ={E}=∗ ∃ q', ▷l ↦∗{q'}: ty_own tid ∗
            (▷l ↦∗{q'}: ty_own tid ={E}=∗ q.[κ] ∗ tl_own tid F)
   }.
@@ -74,22 +74,23 @@ Program Coercion ty_of_st (st : simple_type) : type :=
   |}.
 Next Obligation. intros. apply st_size_eq. Qed.
 Next Obligation.
-  intros st E N κ l tid q ? ?. iIntros "Hmt Htok".
-  iMod (borrow_exists with "Hmt") as (vl) "Hmt". set_solver.
-  iMod (borrow_split with "Hmt") as "[Hmt Hown]". set_solver.
-  iMod (borrow_persistent with "Hown Htok") as "[Hown $]". set_solver.
-  iMod (borrow_fracture with "[Hmt]") as "Hfrac"; last first.
+  intros st E N κ l tid q ? ?. iIntros "#LFT Hmt Htok".
+  iMod (borrow_exists with "LFT Hmt") as (vl) "Hmt". set_solver.
+  iMod (borrow_split with "LFT Hmt") as "[Hmt Hown]". set_solver.
+  iMod (borrow_persistent with "LFT Hown Htok") as "[Hown $]". set_solver.
+  iMod (borrow_fracture with "LFT [Hmt]") as "Hfrac"; last first.
   { iExists vl. by iFrame. }
   done. set_solver.
 Qed.
 Next Obligation.
-  intros st κ κ' tid E E' l ?. iIntros "#Hord H". iDestruct "H" as (vl) "[Hf Hown]".
+  intros st κ κ' tid E E' l ?. iIntros "#LFT #Hord H".
+  iDestruct "H" as (vl) "[Hf Hown]".
   iExists vl. iFrame. by iApply (frac_borrow_shorten with "Hord").
 Qed.
 Next Obligation.
-  intros st κ tid E F l q ??. iIntros "#Hshr[Hlft $]".
+  intros st κ tid E F l q ??. iIntros "#LFT #Hshr[Hlft $]".
   iDestruct "Hshr" as (vl) "[Hf Hown]".
-  iMod (frac_borrow_acc with "[] Hf Hlft") as (q') "[Hmt Hclose]";
+  iMod (frac_borrow_acc with "LFT [] Hf Hlft") as (q') "[Hmt Hclose]";
     first set_solver.
   - iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_vec_op_eq.
     iSplit; auto.
@@ -123,13 +124,13 @@ Section types.
        ty_own tid vl := False%I; ty_shr κ tid E l := False%I |}.
   Next Obligation. iIntros (tid vl) "[]". Qed.
   Next Obligation.
-    iIntros (????????) "Hb Htok".
-    iMod (borrow_exists with "Hb") as (vl) "Hb". set_solver.
-    iMod (borrow_split with "Hb") as "[_ Hb]". set_solver.
-    iMod (borrow_persistent with "Hb Htok") as "[>[] _]". set_solver.
+    iIntros (????????) "#LFT Hb Htok".
+    iMod (borrow_exists with "LFT Hb") as (vl) "Hb". set_solver.
+    iMod (borrow_split with "LFT Hb") as "[_ Hb]". set_solver.
+    iMod (borrow_persistent with "LFT Hb Htok") as "[>[] _]". set_solver.
   Qed.
+  Next Obligation. intros. iIntros "_ _ []". Qed.
   Next Obligation. intros. iIntros "_ []". Qed.
-  Next Obligation. intros. iIntros "[]". Qed.
 
   Program Definition unit : type :=
     {| st_size := 0; st_own tid vl := (vl = [])%I |}.
@@ -162,15 +163,15 @@ Section types.
     iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
   Qed.
   Next Obligation.
-    move=> q ty E N κ l tid q' ?? /=. iIntros "Hshr Htok".
-    iMod (borrow_exists with "Hshr") as (vl) "Hb". set_solver.
-    iMod (borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
-    iMod (borrow_exists with "Hb2") as (l') "Hb2". set_solver.
-    iMod (borrow_split with "Hb2") as "[EQ Hb2]". set_solver.
-    iMod (borrow_persistent with "EQ Htok") as "[>% $]". set_solver. subst.
+    move=> q ty E N κ l tid q' ?? /=. iIntros "#LFT Hshr Htok".
+    iMod (borrow_exists with "LFT Hshr") as (vl) "Hb". set_solver.
+    iMod (borrow_split with "LFT Hb") as "[Hb1 Hb2]". set_solver.
+    iMod (borrow_exists with "LFT Hb2") as (l') "Hb2". set_solver.
+    iMod (borrow_split with "LFT Hb2") as "[EQ Hb2]". set_solver.
+    iMod (borrow_persistent with "LFT EQ Htok") as "[>% $]". set_solver. subst.
     rewrite heap_mapsto_vec_singleton.
-    iMod (borrow_split with "Hb2") as "[Hb2 _]". set_solver.
-    iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "Hb1") as "Hbf". set_solver.
+    iMod (borrow_split with "LFT Hb2") as "[Hb2 _]". set_solver.
+    iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "Hbf". set_solver.
     rewrite /borrow. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
     iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty κ tid N l')%I
          with "[Hpbown]") as "#Hinv"; first by eauto.
@@ -180,15 +181,16 @@ Section types.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - iAssert (&{κ}▷ l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
       { rewrite /borrow. iExists i. eauto. }
-      iMod (borrow_acc_strong with "Hb Htok") as "[Hown Hclose']". set_solver.
+      iMod (borrow_acc_strong with "LFT Hb Htok") as "[Hown Hclose']". set_solver.
       iIntros "!>". iNext.
-      iMod ("Hclose'" with "*[Hown]") as "[Hb Htok]". iFrame. by iIntros "!>[?$]".
-      iMod (ty.(ty_share) with "Hb Htok") as "[#Hshr Htok]"; try done.
+      iMod ("Hclose'" with "*[Hown]") as "[Hb Htok]". iFrame. by iIntros "!>?$".
+      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr Htok]"; try done.
       iMod ("Hclose" with "[]") as "_"; by eauto.
     - iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
   Qed.
   Next Obligation.
-    intros _ ty κ κ' tid E E' l ?. iIntros "#Hκ #H". iDestruct "H" as (l') "[Hfb Hvs]".
+    intros _ ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
+    iDestruct "H" as (l') "[Hfb Hvs]".
     iExists l'. iSplit. by iApply (frac_borrow_shorten with "[]").
     iIntros (q') "!#Htok".
     iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption.
@@ -196,7 +198,7 @@ Section types.
     iMod ("Hvs" $! q'' with "Htok") as "Hvs'".
     iIntros "!>". iNext. iMod "Hvs'" as "[Hshr Htok]".
     iMod ("Hclose" with "Htok"). iFrame.
-    iApply (ty.(ty_shr_mono) with "Hκ"); last done. done.
+    iApply (ty.(ty_shr_mono) with "LFT Hκ"); last done. done.
   Qed.
   Next Obligation. done. Qed.
 
@@ -214,14 +216,14 @@ Section types.
     iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
   Qed.
   Next Obligation.
-    move=> κ ty E N κ' l tid q' ??/=. iIntros "Hshr Htok".
-    iMod (borrow_exists with "Hshr") as (vl) "Hb". set_solver.
-    iMod (borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
-    iMod (borrow_exists with "Hb2") as (l') "Hb2". set_solver.
-    iMod (borrow_split with "Hb2") as "[EQ Hb2]". set_solver.
-    iMod (borrow_persistent with "EQ Htok") as "[>% $]". set_solver. subst.
+    move=> κ ty E N κ' l tid q' ??/=. iIntros "#LFT Hshr Htok".
+    iMod (borrow_exists with "LFT Hshr") as (vl) "Hb". set_solver.
+    iMod (borrow_split with "LFT Hb") as "[Hb1 Hb2]". set_solver.
+    iMod (borrow_exists with "LFT Hb2") as (l') "Hb2". set_solver.
+    iMod (borrow_split with "LFT Hb2") as "[EQ Hb2]". set_solver.
+    iMod (borrow_persistent with "LFT EQ Htok") as "[>% $]". set_solver. subst.
     rewrite heap_mapsto_vec_singleton.
-    iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "Hb1") as "Hbf". set_solver.
+    iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "Hbf". set_solver.
     rewrite {1}/borrow. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
     iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty (κ⋅κ') tid N l')%I
          with "[Hpbown]") as "#Hinv"; first by eauto.
@@ -231,14 +233,14 @@ Section types.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - iAssert (&{κ'}&{κ} l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
       { rewrite /borrow. eauto. }
-      iMod (borrow_unnest with "Hb") as "Hb". set_solver.
+      iMod (borrow_unnest with "LFT Hb") as "Hb". set_solver.
       iIntros "!>". iNext. iMod "Hb".
-      iMod (ty.(ty_share) with "Hb Htok") as "[#Hshr Htok]"; try done.
+      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr Htok]"; try done.
       iMod ("Hclose" with "[]") as "_". eauto. by iFrame.
     - iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
   Qed.
   Next Obligation.
-    intros κ0 ty κ κ' tid E E' l ?. iIntros "#Hκ #H".
+    intros κ0 ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
     iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⋅κ' ⊑ κ0⋅κ) as "#Hκ0".
     { iApply lft_incl_lb. iSplit.
       - iApply lft_le_incl. by exists κ'.
@@ -249,7 +251,7 @@ Section types.
     iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]". set_solver.
     iMod ("Hvs" $! q' with "Htok") as "Hclose'".  iIntros "!>". iNext.
     iMod "Hclose'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
-    iApply (ty_shr_mono with "Hκ0"); last done. done.
+    iApply (ty_shr_mono with "LFT Hκ0"); last done. done.
   Qed.
   Next Obligation. done. Qed.
 
@@ -293,30 +295,30 @@ Section types.
     iDestruct "H1" as %->. iDestruct "H2" as %->. done.
   Qed.
   Next Obligation.
-    intros ty1 ty2 E N κ l tid q ??. iIntros "/=H Htok".
+    intros ty1 ty2 E N κ l tid q ??. iIntros "#LFT /=H Htok".
     rewrite split_prod_mt.
-    iMod (borrow_split with "H") as "[H1 H2]". set_solver.
-    iMod (ty1.(ty_share) _ (N .@ 1) with "H1 Htok") as "[? Htok]". solve_ndisj. done.
-    iMod (ty2.(ty_share) _ (N .@ 2) with "H2 Htok") as "[? $]". solve_ndisj. done.
+    iMod (borrow_split with "LFT H") as "[H1 H2]". set_solver.
+    iMod (ty1.(ty_share) _ (N .@ 1) with "LFT H1 Htok") as "[? Htok]". solve_ndisj. done.
+    iMod (ty2.(ty_share) _ (N .@ 2) with "LFT H2 Htok") as "[? $]". solve_ndisj. done.
     iModIntro. iExists (N .@ 1). iExists (N .@ 2). iFrame.
     iPureIntro. split. solve_ndisj. split; apply nclose_subseteq.
   Qed.
   Next Obligation.
-    intros ty1 ty2 κ κ' tid E E' l ?. iIntros "/=#H⊑ H".
+    intros ty1 ty2 κ κ' tid E E' l ?. iIntros "#LFT /= #H⊑ H".
     iDestruct "H" as (N1 N2) "(% & H1 & H2)". iExists N1, N2.
     iSplit. iPureIntro. set_solver.
-    iSplitL "H1"; by iApply (ty_shr_mono with "H⊑").
+    iSplitL "H1"; by iApply (ty_shr_mono with "LFT H⊑").
   Qed.
   Next Obligation.
     intros ty1 ty2 κ tid E F l q [Hdup1 Hdup2]%andb_True ?.
-    iIntros "H[[Htok1 Htok2] Htl]". iDestruct "H" as (E1 E2) "(% & H1 & H2)".
+    iIntros "#LFT H[[Htok1 Htok2] Htl]". iDestruct "H" as (E1 E2) "(% & H1 & H2)".
     assert (F = E1 ∪ E2 ∪ F∖(E1 ∪ E2)) as ->.
     { rewrite -union_difference_L; set_solver. }
     repeat setoid_rewrite tl_own_union; first last.
     set_solver. set_solver. set_solver. set_solver.
     iDestruct "Htl" as "[[Htl1 Htl2] $]".
-    iMod (ty1.(ty_shr_acc) with "H1 [$Htok1 $Htl1]") as (q1) "[H1 Hclose1]". set_solver.
-    iMod (ty2.(ty_shr_acc) with "H2 [$Htok2 $Htl2]") as (q2) "[H2 Hclose2]". set_solver.
+    iMod (ty1.(ty_shr_acc) with "LFT H1 [$Htok1 $Htl1]") as (q1) "[H1 Hclose1]". set_solver.
+    iMod (ty2.(ty_shr_acc) with "LFT H2 [$Htok2 $Htl2]") as (q2) "[H2 Hclose2]". set_solver.
     destruct (Qp_lower_bound q1 q2) as (qq & q'1 & q'2 & -> & ->). iExists qq.
     iDestruct "H1" as (vl1) "[H↦1 H1]". iDestruct "H2" as (vl2) "[H↦2 H2]".
     rewrite -!heap_mapsto_vec_op_eq !split_prod_mt.
@@ -390,25 +392,25 @@ Section types.
     simpl. by iDestruct (sum_size_eq with "Hown") as %->.
   Qed.
   Next Obligation.
-    intros n tyl Hn E N κ l tid q ??. iIntros "Hown Htok". rewrite split_sum_mt.
-    iMod (borrow_exists with "Hown") as (i) "Hown". set_solver.
-    iMod (borrow_split with "Hown") as "[Hmt Hown]". set_solver.
-    iMod ((nth i tyl emp).(ty_share) with "Hown Htok") as "[#Hshr $]"; try done.
-    iMod (borrow_fracture with "[-]") as "H"; last by eauto. set_solver. iFrame.
+    intros n tyl Hn E N κ l tid q ??. iIntros "#LFT Hown Htok". rewrite split_sum_mt.
+    iMod (borrow_exists with "LFT Hown") as (i) "Hown". set_solver.
+    iMod (borrow_split with "LFT Hown") as "[Hmt Hown]". set_solver.
+    iMod ((nth i tyl emp).(ty_share) with "LFT Hown Htok") as "[#Hshr $]"; try done.
+    iMod (borrow_fracture with "LFT [-]") as "H"; last by eauto. set_solver. iFrame.
   Qed.
   Next Obligation.
-    intros n tyl Hn κ κ' tid E E' l ?. iIntros "#Hord H".
+    intros n tyl Hn κ κ' tid E E' l ?. iIntros "#LFT #Hord H".
     iDestruct "H" as (i) "[Hown0 Hown]". iExists i. iSplitL "Hown0".
     by iApply (frac_borrow_shorten with "Hord").
-    iApply ((nth i tyl emp).(ty_shr_mono) with "Hord"); last done. done.
+    iApply ((nth i tyl emp).(ty_shr_mono) with "LFT Hord"); last done. done.
   Qed.
   Next Obligation.
     intros n tyl Hn κ tid E F l q Hdup%Is_true_eq_true ?.
-    iIntros "#H[[Htok1 Htok2] Htl]".
+    iIntros "#LFT #H[[Htok1 Htok2] Htl]".
     setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 Hshr]".
-    iMod (frac_borrow_acc with "[] Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
+    iMod (frac_borrow_acc with "LFT [] Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
     { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; eauto. }
-    iMod ((nth i tyl emp).(ty_shr_acc) with "Hshr [Htok2 $Htl]")
+    iMod ((nth i tyl emp).(ty_shr_acc) with "LFT Hshr [Htok2 $Htl]")
       as (q'2) "[Hownq Hclose']"; try done.
     { edestruct nth_in_or_default as [| ->]; last done.
       rewrite ->forallb_forall in Hdup. auto using Is_true_eq_left. }
@@ -443,8 +445,8 @@ Section types.
   Next Obligation.
     iIntros (n ρ tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
   Qed.
-  Next Obligation. intros. by iIntros "_ $". Qed.
-  Next Obligation. intros. by iIntros "_ _". Qed.
+  Next Obligation. intros. by iIntros "_ _ $". Qed.
+  Next Obligation. intros. by iIntros "_ _ _". Qed.
   Next Obligation. done. Qed.
 
   (* TODO : For now, functions are not Send. This means they cannot be
diff --git a/theories/type_incl.v b/theories/type_incl.v
index 7f3c825195560f7ce95a9114b53466ed06af6889..e2fdf2af343a3a10518f9cf01a6549e7fff5dcc5 100644
--- a/theories/type_incl.v
+++ b/theories/type_incl.v
@@ -9,7 +9,7 @@ Section ty_incl.
   Context `{iris_typeG Σ}.
 
   Definition ty_incl (ρ : perm) (ty1 ty2 : type) :=
-    ∀ tid, ρ tid ={⊤}=∗
+    ∀ tid, lft_ctx ⊢ ρ tid ={⊤}=∗
       (□ ∀ vl, ty1.(ty_own) tid vl → ty2.(ty_own) tid vl) ∗
       (□ ∀ κ E l, ty1.(ty_shr) κ tid E l →
        (* [ty_incl] needs to prove something about the length of the
@@ -19,14 +19,14 @@ Section ty_incl.
                   ty2.(ty_shr) κ tid E l ∗ ty1.(ty_size) = ty2.(ty_size)).
 
   Global Instance ty_incl_refl ρ : Reflexive (ty_incl ρ).
-  Proof. iIntros (ty tid) "_!>". iSplit; iIntros "!#"; eauto. Qed.
+  Proof. iIntros (ty tid) "__!>". iSplit; iIntros "!#"; eauto. Qed.
 
   Lemma ty_incl_trans ρ θ ty1 ty2 ty3 :
     ty_incl ρ ty1 ty2 → ty_incl θ ty2 ty3 → ty_incl (ρ ∗ θ) ty1 ty3.
   Proof.
-    iIntros (H12 H23 tid) "[H1 H2]".
-    iMod (H12 with "H1") as "[#H12 #H12']".
-    iMod (H23 with "H2") as "[#H23 #H23']".
+    iIntros (H12 H23 tid) "#LFT [H1 H2]".
+    iMod (H12 with "LFT H1") as "[#H12 #H12']".
+    iMod (H23 with "LFT H2") as "[#H23 #H23']".
     iModIntro; iSplit; iIntros "!#*H1".
     - by iApply "H23"; iApply "H12".
     - iDestruct ("H12'" $! _ _ _ with "H1") as "[H2 %]".
@@ -36,7 +36,10 @@ Section ty_incl.
 
   Lemma ty_incl_weaken ρ θ ty1 ty2 :
     ρ ⇒ θ → ty_incl θ ty1 ty2 → ty_incl ρ ty1 ty2.
-  Proof. iIntros (Hρθ Hρ' tid) "H". iMod (Hρθ with "H"). by iApply Hρ'. Qed.
+  Proof.
+    iIntros (Hρθ Hρ' tid) "#LFT H". iMod (Hρθ with "LFT H").
+    by iApply (Hρ' with "LFT").
+  Qed.
 
   Global Instance ty_incl_preorder ρ: Duplicable ρ → PreOrder (ty_incl ρ).
   Proof.
@@ -45,12 +48,12 @@ Section ty_incl.
   Qed.
 
   Lemma ty_incl_emp ρ ty : ty_incl ρ ∅ ty.
-  Proof. iIntros (tid) "_!>". iSplit; iIntros "!#*/=[]". Qed.
+  Proof. iIntros (tid) "_ _!>". iSplit; iIntros "!#*/=[]". Qed.
 
   Lemma ty_incl_own ρ ty1 ty2 q :
     ty_incl ρ ty1 ty2 → ty_incl ρ (own q ty1) (own q ty2).
   Proof.
-    iIntros (Hincl tid) "H/=". iMod (Hincl with "H") as "[#Howni #Hshri]".
+    iIntros (Hincl tid) "#LFT H/=". iMod (Hincl with "LFT H") as "[#Howni #Hshri]".
     iModIntro. iSplit; iIntros "!#*H".
     - iDestruct "H" as (l) "(%&Hmt&H†)". subst. iExists _. iSplit. done.
       iDestruct "Hmt" as (vl') "[Hmt Hown]". iNext.
@@ -68,7 +71,7 @@ Section ty_incl.
   Lemma lft_incl_ty_incl_uniq_borrow ty κ1 κ2 :
     ty_incl (κ1 ⊑ κ2) (&uniq{κ2}ty) (&uniq{κ1}ty).
   Proof.
-    iIntros (tid) "#Hincl!>". iSplit; iIntros "!#*H".
+    iIntros (tid) "#LFT #Hincl!>". iSplit; iIntros "!#*H".
     - iDestruct "H" as (l) "[% Hown]". subst. iExists _. iSplit. done.
       by iApply (borrow_shorten with "Hincl").
     - iAssert (κ1 ⋅ κ ⊑ κ2 ⋅ κ) as "#Hincl'".
@@ -81,19 +84,19 @@ Section ty_incl.
       iMod (lft_incl_acc with "Hincl' Htok") as (q'') "[Htok Hclose]". set_solver.
       iMod ("Hupd" with "*Htok") as "Hupd'". iModIntro. iNext.
       iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
-      by iApply (ty_shr_mono with "Hincl' H").
+      by iApply (ty_shr_mono with "LFT Hincl' H").
   Qed.
 
   Lemma lft_incl_ty_incl_shared_borrow ty κ1 κ2 :
     ty_incl (κ1 ⊑ κ2) (&shr{κ2}ty) (&shr{κ1}ty).
   Proof.
-    iIntros (tid) "#Hincl!>". iSplit; iIntros "!#*H".
+    iIntros (tid) "#LFT #Hincl!>". iSplit; iIntros "!#*H".
     - iDestruct "H" as (l) "(% & H)". subst. iExists _.
-      iSplit. done. by iApply (ty.(ty_shr_mono) with "Hincl").
+      iSplit. done. by iApply (ty.(ty_shr_mono) with "LFT Hincl").
     - iDestruct "H" as (vl) "#[Hfrac Hty]". iSplit; last done.
       iExists vl. iFrame "#". iNext.
       iDestruct "Hty" as (l0) "(% & Hty)". subst. iExists _. iSplit. done.
-      by iApply (ty_shr_mono with "Hincl Hty").
+      by iApply (ty_shr_mono with "LFT Hincl Hty").
   Qed.
 
   (* We have the additional hypothesis that ρ should be duplicable.
@@ -103,8 +106,9 @@ Section ty_incl.
     Duplicable ρ → ty_incl ρ ty11 ty12 → ty_incl ρ ty21 ty22 →
     ty_incl ρ (product2 ty11 ty21) (product2 ty12 ty22).
   Proof.
-    iIntros (Hρ Hincl1 Hincl2 tid) "#Hρ".
-    iMod (Hincl1 with "Hρ") as "[#Ho1#Hs1]". iMod (Hincl2 with "Hρ") as "[#Ho2#Hs2]".
+    iIntros (Hρ Hincl1 Hincl2 tid) "#LFT #Hρ".
+    iMod (Hincl1 with "LFT Hρ") as "[#Ho1#Hs1]".
+    iMod (Hincl2 with "LFT Hρ") as "[#Ho2#Hs2]".
     iSplitL; iIntros "!>!#*H/=".
     - iDestruct "H" as (vl1 vl2) "(% & H1 & H2)". iExists _, _. iSplit. done.
       iSplitL "H1". iApply ("Ho1" with "H1"). iApply ("Ho2" with "H2").
@@ -121,7 +125,7 @@ Section ty_incl.
   Lemma ty_incl_prod2_assoc1 ρ ty1 ty2 ty3 :
     ty_incl ρ (product2 ty1 (product2 ty2 ty3)) (product2 (product2 ty1 ty2) ty3).
   Proof.
-    iIntros (tid) "_!>". iSplit; iIntros "!#/=*H".
+    iIntros (tid) "_ _!>". iSplit; iIntros "!#/=*H".
     - iDestruct "H" as (vl1 vl') "(% & Ho1 & H)".
       iDestruct "H" as (vl2 vl3) "(% & Ho2 & Ho3)". subst.
       iExists _, _. iSplit. by rewrite assoc. iFrame. iExists _, _. by iFrame.
@@ -135,7 +139,7 @@ Section ty_incl.
   Lemma ty_incl_prod2_assoc2 ρ ty1 ty2 ty3 :
     ty_incl ρ (product2 (product2 ty1 ty2) ty3) (product2 ty1 (product2 ty2 ty3)).
   Proof.
-    iIntros (tid) "_!>". iSplit; iIntros "!#/=*H".
+    iIntros (tid) "_ _!>". iSplit; iIntros "!#/=*H".
     - iDestruct "H" as (vl1 vl') "(% & H & Ho3)".
       iDestruct "H" as (vl2 vl3) "(% & Ho1 & Ho2)". subst.
       iExists _, _. iSplit. by rewrite -assoc. iFrame. iExists _, _. by iFrame.
@@ -153,10 +157,10 @@ Section ty_incl.
     apply (ty_incl_weaken _ ⊤). apply perm_incl_top.
     induction tyl1; last by apply (ty_incl_prod2 _ _ _ _ _ _).
     induction tyl2 as [|ty tyl2 IH]; simpl.
-    - iIntros (tid) "_". iSplitL; iIntros "/=!>!#*H".
+    - iIntros (tid) "#LFT _". iSplitL; iIntros "/=!>!#*H".
       + iDestruct "H" as (vl1 vl2) "(% & % & Ho)". subst. done.
       + iDestruct "H" as (E1 E2) "(% & H1 & Ho)". iSplit; last done.
-        rewrite shift_loc_0. iApply (ty_shr_mono with "[] Ho"). set_solver.
+        rewrite shift_loc_0. iApply (ty_shr_mono with "LFT [] Ho"). set_solver.
         iApply lft_incl_refl.
     - etransitivity. apply ty_incl_prod2_assoc2.
       eapply (ty_incl_prod2 _ _ _ _ _ _). done. apply IH.
@@ -169,10 +173,9 @@ Section ty_incl.
     apply (ty_incl_weaken _ ⊤). apply perm_incl_top.
     induction tyl1; last by apply (ty_incl_prod2 _ _ _ _ _ _).
     induction tyl2 as [|ty tyl2 IH]; simpl.
-    - iIntros (tid) "_".
-      iMod (borrow_create with "[]") as "[Hbor _]".
+    - iIntros (tid) "#LFT _". iMod (borrow_create with "LFT []") as "[Hbor _]".
       done. instantiate (1:=True%I). by auto. instantiate (1:=static).
-      iMod (borrow_fracture (λ _, True%I) with "Hbor") as "#Hbor". done.
+      iMod (borrow_fracture (λ _, True%I) with "LFT Hbor") as "#Hbor". done.
       iSplitL; iIntros "/=!>!#*H".
       + iExists [], vl. iFrame. auto.
       + iSplit; last done. iExists ∅, E. iSplit. iPureIntro; set_solver.
@@ -187,27 +190,28 @@ Section ty_incl.
     Duplicable ρ → Forall2 (ty_incl ρ) tyl1 tyl2 →
     ty_incl ρ (sum tyl1) (sum tyl2).
   Proof.
-    iIntros (DUP FA tid) "#Hρ". rewrite /sum /=. iSplitR "".
-    - assert (Hincl : ρ tid ={⊤}=∗
+    iIntros (DUP FA tid) "#LFT #Hρ". rewrite /sum /=. iSplitR "".
+    - assert (Hincl : lft_ctx ⊢ ρ tid ={⊤}=∗
          (□ ∀ i vl, (nth i tyl1 ∅%T).(ty_own) tid vl
                   → (nth i tyl2 ∅%T).(ty_own) tid vl)).
       { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
-        - iIntros "_!>*!#". eauto.
-        - iIntros "#Hρ".  iMod (IH with "Hρ") as "#IH". iMod (Hincl with "Hρ") as "[#Hh _]".
+        - iIntros "_ _!>*!#". eauto.
+        - iIntros "#LFT #Hρ".  iMod (IH with "LFT Hρ") as "#IH".
+          iMod (Hincl with "LFT Hρ") as "[#Hh _]".
           iIntros "!>*!#*Hown". destruct i as [|i]. by iApply "Hh". by iApply "IH". }
-      iMod (Hincl with "Hρ") as "#Hincl". iIntros "!>!#*H".
+      iMod (Hincl with "LFT Hρ") as "#Hincl". iIntros "!>!#*H".
       iDestruct "H" as (i vl') "[% Hown]". subst. iExists _, _. iSplit. done.
         by iApply "Hincl".
-    - assert (Hincl : ρ tid ={⊤}=∗
+    - assert (Hincl : lft_ctx ⊢ ρ tid ={⊤}=∗
          (□ ∀ i κ E l, (nth i tyl1 ∅%T).(ty_shr) κ tid E l
                      → (nth i tyl2 ∅%T).(ty_shr) κ tid E l)).
       { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
-        - iIntros "_!>*!#". eauto.
-        - iIntros "#Hρ".
-          iMod (IH with "Hρ") as "#IH". iMod (Hincl with "Hρ") as "[_ #Hh]".
+        - iIntros "#LFT _!>*!#". eauto.
+        - iIntros "#LFT #Hρ".
+          iMod (IH with "LFT Hρ") as "#IH". iMod (Hincl with "LFT Hρ") as "[_ #Hh]".
           iIntros "!>*!#*Hown". destruct i as [|i]; last by iApply "IH".
           by iDestruct ("Hh" $! _ _ _ with "Hown") as "[$ _]". }
-      iMod (Hincl with "Hρ") as "#Hincl". iIntros "!>!#*H". iSplit; last done.
+      iMod (Hincl with "LFT Hρ") as "#Hincl". iIntros "!>!#*H". iSplit; last done.
       iDestruct "H" as (i) "[??]". iExists _. iSplit. done. by iApply "Hincl".
   Qed.
 
@@ -215,9 +219,9 @@ Section ty_incl.
     Duplicable ρ → (∀ vl : vec val n, ρ ∗ ρ2 vl ⇒ ρ1 vl) →
     ty_incl ρ (cont ρ1) (cont ρ2).
   Proof.
-    iIntros (? Hρ1ρ2 tid) "#Hρ!>". iSplit; iIntros "!#*H"; last by auto.
+    iIntros (? Hρ1ρ2 tid) "#LFT #Hρ!>". iSplit; iIntros "!#*H"; last by auto.
     iDestruct "H" as (f) "[% Hwp]". subst. iExists _. iSplit. done.
-    iIntros (vl) "Hρ2 Htl". iMod (Hρ1ρ2 with "[Hρ2]"). by iFrame.
+    iIntros (vl) "Hρ2 Htl". iMod (Hρ1ρ2 with "LFT [$Hρ2 $Hρ]").
     by iApply ("Hwp" with "[-Htl] Htl").
   Qed.
 
@@ -225,21 +229,21 @@ Section ty_incl.
     Duplicable ρ → (∀ (x : A) (vl : vec val n), ρ ∗ ρ2 x vl ⇒ ρ1 x vl) →
     ty_incl ρ (fn ρ1) (fn ρ2).
   Proof.
-    iIntros (? Hρ1ρ2 tid) "#Hρ!>". iSplit; iIntros "!#*#H".
+    iIntros (? Hρ1ρ2 tid) "#LFT #Hρ!>". iSplit; iIntros "!#*#H".
     - iDestruct "H" as (f) "[% Hwp]". subst. iExists _. iSplit. done.
-      iIntros (x vl) "!#[Hρ2 Htl]". iMod (Hρ1ρ2 with "[Hρ2]"). by iFrame.
+      iIntros (x vl) "!#[Hρ2 Htl]". iMod (Hρ1ρ2 with "LFT [$Hρ2 $Hρ]").
       iApply "Hwp". by iFrame.
     - iSplit; last done. simpl. iDestruct "H" as (vl0) "[? Hvl]".
       iExists vl0. iFrame "#". iNext. iDestruct "Hvl" as (f) "[% Hwp]".
       iExists f. iSplit. done.
-      iIntros (x vl) "!#[Hρ2 Htl]". iMod (Hρ1ρ2 with "[Hρ2]"). by iFrame.
+      iIntros (x vl) "!#[Hρ2 Htl]". iMod (Hρ1ρ2 with "LFT [$Hρ2 $Hρ]").
       iApply "Hwp". by iFrame.
   Qed.
 
   Lemma ty_incl_fn_cont {A n} ρ ρf (x : A) :
     ty_incl ρ (fn ρf) (cont (n:=n) (ρf x)).
   Proof.
-    iIntros (tid) "_!>". iSplit; iIntros "!#*H"; last by iSplit.
+    iIntros (tid) "#LFT _!>". iSplit; iIntros "!#*H"; last by iSplit.
     iDestruct "H" as (f) "[%#H]". subst. iExists _. iSplit. done.
     iIntros (vl) "Hρf Htl". iApply "H". by iFrame.
   Qed.
@@ -247,7 +251,7 @@ Section ty_incl.
   Lemma ty_incl_fn_specialize {A B n} (f : A → B) ρ ρfn :
     ty_incl ρ (fn (n:=n) ρfn) (fn (ρfn ∘ f)).
   Proof.
-    iIntros (tid) "_!>". iSplit; iIntros "!#*H".
+    iIntros (tid) "_ _!>". iSplit; iIntros "!#*H".
     - iDestruct "H" as (fv) "[%#H]". subst. iExists _. iSplit. done.
       iIntros (x vl). by iApply "H".
     - iSplit; last done.
@@ -259,7 +263,7 @@ Section ty_incl.
   Lemma ty_incl_perm_incl ρ ty1 ty2 ν :
     ty_incl ρ ty1 ty2 → ρ ∗ ν ◁ ty1 ⇒ ν ◁ ty2.
   Proof.
-    iIntros (Hincl tid) "[Hρ Hty1]". iMod (Hincl with "Hρ") as "[#Hownincl _]".
+    iIntros (Hincl tid) "#LFT [Hρ Hty1]". iMod (Hincl with "LFT Hρ") as "[#Hownincl _]".
     unfold Perm.has_type. destruct (Perm.eval_expr ν); last done. by iApply "Hownincl".
   Qed.
 
diff --git a/theories/typing.v b/theories/typing.v
index c78fec77faad380bea82b986fc81582b8f2a1177..bf0398bf219a0eabc4ffe3958671c293c70740da 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -11,35 +11,35 @@ Section typing.
 
   (* TODO : good notations for [typed_step] and [typed_step_ty] ? *)
   Definition typed_step (ρ : perm) e (θ : val → perm) :=
-    ∀ tid, {{ heap_ctx ∗ ρ tid ∗ tl_own tid ⊤ }} e
+    ∀ tid, {{ heap_ctx ∗ lft_ctx ∗ ρ tid ∗ tl_own tid ⊤ }} e
            {{ v, θ v tid ∗ tl_own tid ⊤ }}.
 
   Definition typed_step_ty (ρ : perm) e ty :=
     typed_step ρ e (λ ν, ν ◁ ty)%P.
 
   Definition typed_program (ρ : perm) e :=
-    ∀ tid, {{ heap_ctx ∗ ρ tid ∗ tl_own tid ⊤ }} e {{ _, False }}.
+    ∀ tid, {{ heap_ctx ∗ lft_ctx ∗ ρ tid ∗ tl_own tid ⊤ }} e {{ _, False }}.
 
   Lemma typed_frame ρ e θ ξ:
     typed_step ρ e θ → typed_step (ρ ∗ ξ) e (λ ν, θ ν ∗ ξ)%P.
   Proof.
-    iIntros (Hwt tid) "!#(#HEAP&[?$]&?)". iApply Hwt. by iFrame.
+    iIntros (Hwt tid) "!#(#HEAP&#LFT&[?$]&?)". iApply Hwt. iFrame "∗#".
   Qed.
 
   Lemma typed_step_exists {A} ρ θ e ξ:
     (∀ x:A, typed_step (ρ ∗ θ x) e ξ) →
     typed_step (ρ ∗ ∃ x, θ x) e ξ.
   Proof.
-    iIntros (Hwt tid) "!#(#HEAP&[Hρ Hθ]&?)". iDestruct "Hθ" as (x) "Hθ".
-    iApply Hwt. by iFrame.
+    iIntros (Hwt tid) "!#(#HEAP&#LFT&[Hρ Hθ]&?)". iDestruct "Hθ" as (x) "Hθ".
+    iApply Hwt. iFrame "∗#".
   Qed.
 
   Lemma typed_bool ρ (b:Datatypes.bool): typed_step_ty ρ #b bool.
-  Proof. iIntros (tid) "!#(_&_&$)". wp_value. by iExists _. Qed.
+  Proof. iIntros (tid) "!#(_&_&_&$)". wp_value. by iExists _. Qed.
 
   Lemma typed_int ρ (z:Datatypes.nat) :
     typed_step_ty ρ #z int.
-  Proof. iIntros (tid) "!#(_&_&$)". wp_value. by iExists _. Qed.
+  Proof. iIntros (tid) "!#(_&_&_&$)". wp_value. by iExists _. Qed.
 
   Lemma typed_fn {A n} `{Duplicable _ ρ, Closed (f :b: xl +b+ []) e} θ :
     length xl = n →
@@ -48,7 +48,7 @@ Section typing.
         typed_program (fv ◁ fn θ ∗ (θ a vl) ∗ ρ) (subst' f fv e')) →
     typed_step_ty ρ (Rec f xl e) (fn θ).
   Proof.
-    iIntros (Hn He tid) "!#(#HEAP&#Hρ&$)".
+    iIntros (Hn He tid) "!#(#HEAP&#LFT&#Hρ&$)".
     assert (Rec f xl e = RecV f xl e) as -> by done. iApply wp_value'.
     rewrite has_type_value.
     iLöb as "IH". iExists _. iSplit. done. iIntros (a vl) "!#[Hθ?]".
@@ -68,7 +68,7 @@ Section typing.
         typed_program (fv ◁ cont (λ vl, ρ ∗ θ vl)%P ∗ (θ vl) ∗ ρ) (subst' f fv e')) →
     typed_step_ty ρ (Rec f xl e) (cont θ).
   Proof.
-    iIntros (Hn He tid) "!#(#HEAP&Hρ&$)". specialize (He (RecV f xl e)).
+    iIntros (Hn He tid) "!#(#HEAP&#LFT&Hρ&$)". specialize (He (RecV f xl e)).
     assert (Rec f xl e = RecV f xl e) as -> by done. iApply wp_value'.
     rewrite has_type_value.
     iLöb as "IH". iExists _. iSplit. done. iIntros (vl) "Hθ ?".
@@ -87,7 +87,7 @@ Section typing.
   Lemma typed_valuable (ν : expr) ty:
     typed_step_ty (ν ◁ ty) ν ty.
   Proof.
-    iIntros (tid) "!#(_&H&$)". iApply (has_type_wp with "[$H]"). by iIntros (v) "[_$]".
+    iIntros (tid) "!#(_&_&H&$)". iApply (has_type_wp with "[$H]"). by iIntros (v) "[_$]".
   Qed.
 
   Lemma typed_plus e1 e2 ρ1 ρ2:
@@ -95,10 +95,10 @@ Section typing.
     typed_step_ty (ρ1 ∗ ρ2) (e1 + e2) int.
   Proof.
     unfold typed_step_ty, typed_step. setoid_rewrite has_type_value.
-    iIntros (He1 He2 tid) "!#(#HEAP&[H1 H2]&?)".
-    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; by iFrame.
+    iIntros (He1 He2 tid) "!#(#HEAP&#ĽFT&[H1 H2]&?)".
+    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; iFrame "∗#".
     iIntros (v1) "[Hv1?]". iDestruct "Hv1" as (z1) "Hz1". iDestruct "Hz1" as %[=->].
-    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; by iFrame.
+    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; iFrame "∗#".
     iIntros (v2) "[Hv2$]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
     wp_op. by iExists _.
   Qed.
@@ -108,10 +108,10 @@ Section typing.
     typed_step_ty (ρ1 ∗ ρ2) (e1 - e2) int.
   Proof.
     unfold typed_step_ty, typed_step. setoid_rewrite has_type_value.
-    iIntros (He1 He2 tid) "!#(#HEAP&[H1 H2]&?)".
-    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; by iFrame.
+    iIntros (He1 He2 tid) "!#(#HEAP&#LFT&[H1 H2]&?)".
+    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; iFrame "∗#".
     iIntros (v1) "[Hv1?]". iDestruct "Hv1" as (z1) "Hz1". iDestruct "Hz1" as %[=->].
-    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; by iFrame.
+    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; iFrame "∗#".
     iIntros (v2) "[Hv2$]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
     wp_op. by iExists _.
   Qed.
@@ -121,10 +121,10 @@ Section typing.
     typed_step_ty (ρ1 ∗ ρ2) (e1 ≤ e2) bool.
   Proof.
     unfold typed_step_ty, typed_step. setoid_rewrite has_type_value.
-    iIntros (He1 He2 tid) "!#(#HEAP&[H1 H2]&?)".
-    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; by iFrame.
+    iIntros (He1 He2 tid) "!#(#HEAP&#LFT&[H1 H2]&?)".
+    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; iFrame "∗#".
     iIntros (v1) "[Hv1?]". iDestruct "Hv1" as (z1) "Hz1". iDestruct "Hz1" as %[=->].
-    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; by iFrame.
+    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; iFrame "∗#".
     iIntros (v2) "[Hv2$]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
     wp_op; intros _; by iExists _.
   Qed.
@@ -132,14 +132,15 @@ Section typing.
   Lemma typed_newlft ρ:
     typed_step ρ Newlft (λ _, ∃ α, 1.[α] ∗ α ∋ top)%P.
   Proof.
-    iIntros (tid) "!#(_&_&$)". wp_value. iMod lft_create as (α) "[?#?]". done.
+    iIntros (tid) "!#(_&#LFT&_&$)". wp_value.
+    iMod (lft_create with "LFT") as (α) "[?#?]". done.
     iExists α. iFrame. iIntros "!>_!>". done.
   Qed.
 
   Lemma typed_endlft κ ρ:
     typed_step (κ ∋ ρ ∗ 1.[κ] ∗ †κ) Endlft (λ _, ρ)%P.
   Proof.
-    iIntros (tid) "!#(_&(Hextr&Htok&Hend)&$)".
+    iIntros (tid) "!#(_&_&(Hextr&Htok&Hend)&$)".
     iApply wp_fupd. iApply (wp_wand_r _ _ (λ _, _ ∗ True)%I). iSplitR "Hextr".
     iApply (wp_frame_step_l with "[-]"); try done.
     iDestruct ("Hend" with "Htok") as "$". by wp_seq.
@@ -149,7 +150,7 @@ Section typing.
   Lemma typed_alloc ρ (n : nat):
     0 < n → typed_step_ty ρ (Alloc #n) (own 1 (Π(replicate n uninit))).
   Proof.
-    iIntros (Hn tid) "!#(#HEAP&_&$)". wp_alloc l vl as "H↦" "H†". iIntros "!>".
+    iIntros (Hn tid) "!#(#HEAP&_&_&$)". wp_alloc l vl as "H↦" "H†". iIntros "!>".
     iExists _. iSplit. done. iNext. rewrite Nat2Z.id. iSplitR "H†".
     - iExists vl. iFrame.
       match goal with H : Z.of_nat n = Z.of_nat (length vl) |- _ => rename H into Hlen end.
@@ -163,7 +164,7 @@ Section typing.
   Lemma typed_free ty (ν : expr):
     typed_step (ν ◁ own 1 ty) (Free #ty.(ty_size) ν) (λ _, top).
   Proof.
-    iIntros (tid) "!#(#HEAP&H◁&$)". wp_bind ν.
+    iIntros (tid) "!#(#HEAP&_&H◁&$)". wp_bind ν.
     iApply (has_type_wp with "[$H◁]"). iIntros (v) "[_ H◁]!>".
     rewrite has_type_value.
     iDestruct "H◁" as (l) "(Hv & H↦∗: & >H†)". iDestruct "Hv" as %[=->].
@@ -173,17 +174,17 @@ Section typing.
 
   Definition consumes (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
     ∀ ν tid Φ E, mgmtE ∪ lrustN ⊆ E →
-      ρ1 ν tid ∗ tl_own tid ⊤ ∗
+      lft_ctx ⊢ ρ1 ν tid -∗ tl_own tid ⊤ -∗
       (∀ (l:loc) vl q,
         (length vl = ty.(ty_size) ∗ eval_expr ν = Some #l ∗ l ↦∗{q} vl ∗
          |={E}▷=> (ty.(ty_own) tid vl ∗ (l ↦∗{q} vl ={E}=∗ ρ2 ν tid ∗ tl_own tid ⊤)))
        -∗ Φ #l)
-      ⊢ WP ν @ E {{ Φ }}.
+      -∗ WP ν @ E {{ Φ }}.
 
   Lemma consumes_copy_own ty q:
     ty.(ty_dup) → consumes ty (λ ν, ν ◁ own q ty)%P (λ ν, ν ◁ own q ty)%P.
   Proof.
-    iIntros (? ν tid Φ E ?) "(H◁ & Htl & HΦ)". iApply (has_type_wp with "[- $H◁]").
+    iIntros (? ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "[- $H◁]").
     iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦ & >H†)".
     iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ #Hown]".
@@ -197,7 +198,7 @@ Section typing.
     consumes ty (λ ν, ν ◁ own q ty)%P
              (λ ν, ν ◁ own q (Π(replicate ty.(ty_size) uninit)))%P.
   Proof.
-    iIntros (ν tid Φ E ?) "(H◁ & Htl & HΦ)". iApply (has_type_wp with "[- $H◁]").
+    iIntros (ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "[- $H◁]").
     iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦ & >H†)".
     iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
@@ -217,11 +218,11 @@ Section typing.
     consumes ty (λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
                 (λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
-    iIntros (? ν tid Φ E ?) "((H◁ & #H⊑ & Htok) & Htl & HΦ)".
+    iIntros (? ν tid Φ E ?) "#LFT (H◁ & #H⊑ & Htok) Htl HΦ".
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l') "[Heq H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
-    iMod (borrow_acc with "H↦ Htok") as "[H↦ Hclose']". set_solver.
+    iMod (borrow_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
     iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
       by rewrite ty.(ty_size_eq).
@@ -235,13 +236,13 @@ Section typing.
     consumes ty (λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
                 (λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
-    iIntros (? ν tid Φ E ?) "((H◁ & #H⊑ & Htok) & Htl & HΦ)".
+    iIntros (? ν tid Φ E ?) "#LFT (H◁ & #H⊑ & Htok) Htl HΦ".
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l') "[Heq #Hshr]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
     rewrite (union_difference_L (nclose lrustN) ⊤); last done.
     setoid_rewrite ->tl_own_union; try set_solver. iDestruct "Htl" as "[Htl ?]".
-    iMod (ty_shr_acc with "Hshr [$Htok $Htl]") as (q'') "[H↦ Hclose']"; try set_solver.
+    iMod (ty_shr_acc with "LFT Hshr [$Htok $Htl]") as (q'') "[H↦ Hclose']"; try set_solver.
     iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
       by rewrite ty.(ty_size_eq).
@@ -254,8 +255,8 @@ Section typing.
     ty.(ty_size) = 1%nat → consumes ty ρ1 ρ2 →
     typed_step (ρ1 ν) (!ν) (λ v, v ◁ ty ∗ ρ2 ν)%P.
   Proof.
-    iIntros (Hsz Hconsumes tid) "!#[#HEAP[??]]". wp_bind ν.
-    iApply Hconsumes. done. iFrame. iIntros (l vl q) "(%&%&H↦&>Hupd)".
+    iIntros (Hsz Hconsumes tid) "!#(#HEAP & #LFT & Hρ1 & Htl)". wp_bind ν.
+    iApply (Hconsumes with "LFT Hρ1 Htl"). done. iFrame. iIntros (l vl q) "(%&%&H↦&>Hupd)".
     rewrite ->Hsz in *. destruct vl as [|v [|]]; try done.
     rewrite heap_mapsto_vec_singleton. wp_read. rewrite /sep has_type_value.
     iMod "Hupd" as "[$ Hclose]". by iApply "Hclose".
@@ -266,18 +267,18 @@ Section typing.
                (!ν)
                (λ v, v ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
-    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑ & Htok) & $)". wp_bind ν.
+    iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑ & Htok) & $)". wp_bind ν.
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
-    iMod (borrow_acc_strong with "H↦ Htok") as "[H↦ Hclose']". done.
+    iMod (borrow_acc_strong with "LFT H↦ Htok") as "[H↦ Hclose']". done.
     iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct "Hown" as (l') "(>% & Hown & H†)".
     subst. rewrite heap_mapsto_vec_singleton. wp_read.
     iMod ("Hclose'" with "*[H↦ Hown H†]") as "[Hbor Htok]"; last first.
-    - iMod (borrow_split with "Hbor") as "[_ Hbor]". done.
-      iMod (borrow_split with "Hbor") as "[_ Hbor]". done.
+    - iMod (borrow_split with "LFT Hbor") as "[_ Hbor]". done.
+      iMod (borrow_split with "LFT Hbor") as "[_ Hbor]". done.
       iMod ("Hclose" with "Htok") as "$". iFrame "#". iExists _. eauto.
-    - iIntros "{$H↦ $H† $Hown}!>[_(?&?&?)]!>". iNext. iExists _.
+    - iIntros "{$H↦ $H† $Hown}!>_(?&?&?)!>". iNext. iExists _.
       rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
   Qed.
 
@@ -286,12 +287,12 @@ Section typing.
                (!ν)
                (λ v, v ◁ &shr{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
-    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑ & Htok) & $)". wp_bind ν.
+    iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑ & Htok) & $)". wp_bind ν.
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
     iDestruct "H↦" as (vl) "[H↦b Hown]".
-    iMod (frac_borrow_acc with "[] H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
+    iMod (frac_borrow_acc with "LFT [] H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
     { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
     iSpecialize ("Hown" $! _ with "Htok2").
     iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose'"; last first.
@@ -310,17 +311,17 @@ Section typing.
                (!ν)
                (λ v, v ◁ &uniq{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
   Proof.
-    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑1 & Htok & #H⊑2) & $)". wp_bind ν.
+    iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑1 & Htok & #H⊑2) & $)". wp_bind ν.
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑1 Htok") as (q'') "[Htok Hclose]". done.
-    iMod (borrow_exists with "H↦") as (vl) "Hbor". done.
-    iMod (borrow_split with "Hbor") as "[H↦ Hbor]". done.
-    iMod (borrow_exists with "Hbor") as (l') "Hbor". done.
-    iMod (borrow_split with "Hbor") as "[Heq Hbor]". done.
-    iMod (borrow_unnest with "Hbor") as "Hbor". done.
-    iMod (borrow_persistent with "Heq Htok") as "[>% Htok]". done. subst.
-    iMod (borrow_acc with "H↦ Htok") as "[>H↦ Hclose']". done.
+    iMod (borrow_exists with "LFT H↦") as (vl) "Hbor". done.
+    iMod (borrow_split with "LFT Hbor") as "[H↦ Hbor]". done.
+    iMod (borrow_exists with "LFT Hbor") as (l') "Hbor". done.
+    iMod (borrow_split with "LFT Hbor") as "[Heq Hbor]". done.
+    iMod (borrow_unnest with "LFT Hbor") as "Hbor". done.
+    iMod (borrow_persistent with "LFT Heq Htok") as "[>% Htok]". done. subst.
+    iMod (borrow_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
     rewrite heap_mapsto_vec_singleton. wp_read.
     iMod ("Hclose'" with "[$H↦]") as "[H↦ Htok]".
     iMod ("Hclose" with "Htok") as "$". iFrame "#".
@@ -333,12 +334,12 @@ Section typing.
                (!ν)
                (λ v, v ◁ &shr{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
   Proof.
-    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑1 & Htok & #H⊑2) & $)". wp_bind ν.
+    iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑1 & Htok & #H⊑2) & $)". wp_bind ν.
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq Hshr]".
     iDestruct "Heq" as %[=->]. iDestruct "Hshr" as (l') "[H↦ Hown]".
     iMod (lft_incl_acc with "H⊑1 Htok") as (q') "[[Htok1 Htok2] Hclose]". done.
-    iMod (frac_borrow_acc with "[] H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
+    iMod (frac_borrow_acc with "LFT [] H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
     { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
     iAssert (κ' ⊑ κ'' ⋅ κ') as "#H⊑3".
     { iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
@@ -353,23 +354,23 @@ Section typing.
       iMod ("Hclose''" with "Htok") as "Htok".
       iMod ("Hclose'" with "[$H↦]") as "Htok'".
       iMod ("Hclose" with "[$Htok $Htok']") as "$". iFrame "#". iExists _.
-      iSplitL. done. by iApply (ty_shr_mono with "H⊑3 Hshr").
+      iSplitL. done. by iApply (ty_shr_mono with "LFT H⊑3 Hshr").
   Qed.
 
   Definition update (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
     ∀ ν tid Φ E, mgmtE ∪ lrustN ⊆ E →
-      ρ1 ν tid ∗
+      lft_ctx ⊢ ρ1 ν tid -∗
       (∀ (l:loc) vl,
          (length vl = ty.(ty_size) ∗ eval_expr ν = Some #l ∗ l ↦∗ vl ∗
          ∀ vl', l ↦∗ vl' ∗ ▷ (ty.(ty_own) tid vl') ={E}=∗ ρ2 ν tid)
          -∗ Φ #l)
-      ⊢ WP ν @ E {{ Φ }}.
+      -∗ WP ν @ E {{ Φ }}.
 
   Lemma update_strong ty1 ty2 q:
     ty1.(ty_size) = ty2.(ty_size) →
     update ty1 (λ ν, ν ◁ own q ty2)%P (λ ν, ν ◁ own q ty1)%P.
   Proof.
-    iIntros (Hsz ν tid Φ E ?) "[H◁ HΦ]". iApply (has_type_wp with "[- $H◁]").
+    iIntros (Hsz ν tid Φ E ?) "_ H◁ HΦ". iApply (has_type_wp with "[- $H◁]").
     iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦ & >H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
@@ -382,11 +383,11 @@ Section typing.
     update ty (λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
               (λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
-    iIntros (ν tid Φ E ?) "[(H◁ & #H⊑ & Htok) HΦ]".
+    iIntros (ν tid Φ E ?) "#LFT (H◁ & #H⊑ & Htok) HΦ".
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦)". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
-    iMod (borrow_acc with "H↦ Htok") as "[H↦ Hclose']". set_solver.
+    iMod (borrow_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
     iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
     iDestruct "Hown" as ">%". iApply "HΦ". iFrame "∗%#". iIntros (vl') "[H↦ Hown]".
     iMod ("Hclose'" with "[H↦ Hown]") as "[Hbor Htok]". by iExists _; iFrame.
@@ -397,8 +398,8 @@ Section typing.
     ty.(ty_size) = 1%nat → update ty ρ1 ρ2 →
     typed_step (ρ1 ν1 ∗ ν2 ◁ ty) (ν1 <- ν2) (λ _, ρ2 ν1).
   Proof.
-    iIntros (Hsz Hupd tid) "!#(#HEAP & [Hρ1 H◁] & $)". wp_bind ν1.
-    iApply Hupd. done. iFrame. iIntros (l vl) "(%&%&H↦&Hupd)".
+    iIntros (Hsz Hupd tid) "!#(#HEAP & #LFT & [Hρ1 H◁] & $)". wp_bind ν1.
+    iApply (Hupd with "LFT Hρ1"). done. iFrame. iIntros (l vl) "(%&%&H↦&Hupd)".
     rewrite ->Hsz in *. destruct vl as [|v[|]]; try done.
     wp_bind ν2. iApply (has_type_wp with "[- $H◁]"). iIntros (v') "[% H◁]!>".
     rewrite heap_mapsto_vec_singleton. wp_write.
@@ -409,10 +410,10 @@ Section typing.
     update ty ρ1' ρ1 → consumes ty ρ2' ρ2 →
     typed_step (ρ1' ν1 ∗ ρ2' ν2) (ν1 <-{ty.(ty_size)} !ν2) (λ _, ρ1 ν1 ∗ ρ2 ν2)%P.
   Proof.
-    iIntros (Hupd Hcons tid) "!#(#HEAP&[H1 H2]&Htl)". wp_bind ν1.
-    iApply (Hupd with "[- $H1]"). done.
+    iIntros (Hupd Hcons tid) "!#(#HEAP & #LFT & [H1 H2] & Htl)". wp_bind ν1.
+    iApply (Hupd with "LFT H1"). done.
     iIntros (l vl) "(% & % & H↦ & Hupd)". wp_bind ν2.
-    iApply (Hcons with "[- $H2 $Htl]"). done.
+    iApply (Hcons with "LFT H2 Htl"). done.
     iIntros (l' vl' q) "(% & % & H↦' & Hcons)". iApply wp_fupd.
     iMod "Hcons". iApply (wp_memcpy with "[$HEAP $H↦' $H↦]"); try done. iNext.
     iIntros "[H↦ H↦']". iMod "Hcons" as "[Hown' Hcons]".
@@ -422,16 +423,16 @@ Section typing.
   Lemma typed_weaken ρ1 ρ2 e:
     typed_program ρ2 e → (ρ1 ⇒ ρ2) → typed_program ρ1 e.
   Proof.
-    iIntros (Hρ2 Hρ12 tid) "!#(#HEAP & Hρ1 & Htl)".
-    iMod (Hρ12 with "Hρ1"). iApply Hρ2. by iFrame.
+    iIntros (Hρ2 Hρ12 tid) "!#(#HEAP & #LFT & Hρ1 & Htl)".
+    iMod (Hρ12 with "LFT Hρ1"). iApply Hρ2. iFrame "∗#".
   Qed.
 
   Lemma typed_program_exists {A} ρ θ e:
     (∀ x:A, typed_program (ρ ∗ θ x) e) →
     typed_program (ρ ∗ ∃ x, θ x) e.
   Proof.
-    iIntros (Hwt tid) "!#(#HEAP & [Hρ Hθ] & ?)". iDestruct "Hθ" as (x) "Hθ".
-    iApply Hwt. by iFrame.
+    iIntros (Hwt tid) "!#(#HEAP & #LFT & [Hρ Hθ] & ?)". iDestruct "Hθ" as (x) "Hθ".
+    iApply Hwt. iFrame "∗#".
   Qed.
 
   Lemma typed_step_program ρ θ e K:
@@ -439,19 +440,19 @@ Section typing.
     (∀ v, typed_program (θ v) (fill K (of_val v))) →
     typed_program ρ (fill K e).
   Proof.
-    iIntros (He HK tid) "!#(#HEAP & Hρ & Htl)".
-    iApply wp_bind. iApply wp_wand_r. iSplitL. iApply He; by iFrame.
-    iIntros (v) "[Hθ Htl]". iApply HK. by iFrame.
+    iIntros (He HK tid) "!#(#HEAP & #LFT & Hρ & Htl)".
+    iApply wp_bind. iApply wp_wand_r. iSplitL. iApply He; iFrame "∗#".
+    iIntros (v) "[Hθ Htl]". iApply HK. iFrame "∗#".
   Qed.
 
   Lemma typed_if ρ e1 e2 ν:
     typed_program ρ e1 → typed_program ρ e2 →
     typed_program (ρ ∗ ν ◁ bool) (if: ν then e1 else e2).
   Proof.
-    iIntros (He1 He2 tid) "!#(#HEAP & [Hρ H◁] & Htl)".
+    iIntros (He1 He2 tid) "!#(#HEAP & #LFT & [Hρ H◁] & Htl)".
     wp_bind ν. iApply has_type_wp. iFrame. iIntros (v) "[% H◁]!>".
     rewrite has_type_value. iDestruct "H◁" as (b) "Heq". iDestruct "Heq" as %[= ->].
-    wp_if. destruct b; iNext. iApply He1; by iFrame. iApply He2; by iFrame.
+    wp_if. destruct b; iNext. iApply He1; iFrame "∗#". iApply He2; iFrame "∗#".
   Qed.
 
 End typing.