diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 0c9d3409bcf51bf25226e47832f77edad5253b85..983f27861faf86a8f818bf0fb6e51cf59d585e50 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -5,14 +5,14 @@ Set Default Proof Using "Type".
 
 (** Atomic persistent bors  *)
 (* TODO : update the TEX with the fact that we can choose the namespace. *)
-Definition at_bor `{!invG Σ, !lftG Σ} κ N (P : iProp Σ) :=
+Definition at_bor `{!invG Σ, !lftG Σ userE} κ N (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗
     (⌜N ## lftN⌝ ∗ inv N (idx_bor_own 1 i) ∨
      ⌜N = lftN⌝ ∗ inv N (∃ q, idx_bor_own q i)))%I.
 Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : bi_scope.
 
 Section atomic_bors.
-  Context `{!invG Σ, !lftG Σ} (P : iProp Σ) (N : namespace).
+  Context `{!invG Σ, !lftG Σ userE} (P : iProp Σ) (N : namespace).
 
   Global Instance at_bor_ne κ n : Proper (dist n ==> dist n) (at_bor κ N).
   Proof. solve_proper. Qed.
@@ -97,7 +97,7 @@ Section atomic_bors.
   Qed.
 End atomic_bors.
 
-Lemma at_bor_acc_lftN `{!invG Σ, !lftG Σ} (P : iProp Σ) E κ :
+Lemma at_bor_acc_lftN `{!invG Σ, !lftG Σ userE} (P : iProp Σ) E κ :
   ↑lftN ⊆ E →
   lft_ctx -∗ &at{κ,lftN}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
              [†κ] ∗ |={E∖↑lftN,E}=> True.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 94aa2a3cb06363d301565d1f468427abc8f930ac..3f04c378e71ab60e5d0bcf3b53777caf499f6a45 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -6,15 +6,16 @@ Set Default Proof Using "Type".
 
 Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
 
-Local Definition frac_bor_inv `{!invG Σ, !lftG Σ, !frac_borG Σ} (φ : Qp → iProp Σ) γ κ' :=
+Local Definition frac_bor_inv `{!invG Σ, !lftG Σ userE, !frac_borG Σ}
+                              (φ : Qp → iProp Σ) γ κ' :=
   (∃ q, φ q ∗ own γ q ∗ (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ']))%I.
 
-Definition frac_bor `{!invG Σ, !lftG Σ, !frac_borG Σ} κ (φ : Qp → iProp Σ) :=
+Definition frac_bor `{!invG Σ, !lftG Σ userE, !frac_borG Σ} κ (φ : Qp → iProp Σ) :=
   (∃ γ κ', κ ⊑ κ' ∗ &at{κ',lftN} (frac_bor_inv φ γ κ'))%I.
 Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : bi_scope.
 
 Section frac_bor.
-  Context `{!invG Σ, !lftG Σ, !frac_borG Σ} (φ : Qp → iProp Σ).
+  Context `{!invG Σ, !lftG Σ userE, !frac_borG Σ} (φ : Qp → iProp Σ).
   Implicit Types E : coPset.
 
   Global Instance frac_bor_contractive κ n :
@@ -154,7 +155,7 @@ Section frac_bor.
   Qed.
 End frac_bor.
 
-Lemma frac_bor_lft_incl `{!invG Σ, !lftG Σ, !frac_borG Σ} κ κ' q:
+Lemma frac_bor_lft_incl `{!invG Σ, !lftG Σ userE, !frac_borG Σ} κ κ' q:
   lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
 Proof.
   iIntros "#LFT#Hbor". iApply lft_incl_intro. iModIntro. iSplitR.
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 9053aaac6afc2c48f4474ce9a51919d6de1b44d6..ace6b15d9b663ae424b64a50b209455a3dbf55de 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -26,12 +26,12 @@ Definition lft_incl_syntactic (κ κ' : lft) : Prop := ∃ κ'', κ'' ⊓ κ' =
 Infix "⊑ˢʸⁿ" := lft_incl_syntactic (at level 40) : stdpp_scope.
 
 Section derived.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invG Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 Lemma lft_create E :
   ↑lftN ⊆ E →
-  lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†κ]).
+  lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ userE}[userE]▷=∗ [†κ]).
 Proof.
   iIntros (?) "#LFT".
   iMod (lft_create_strong (λ _, True) with "LFT") as (κ _) "H"=>//;
@@ -50,7 +50,7 @@ Qed.
 Lemma bor_acc_atomic_cons E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
-    (▷ P ∗ ∀ Q, ▷ (▷ Q ={↑lft_userN}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ} Q) ∨
+    (▷ P ∗ ∀ Q, ▷ (▷ Q ={userE}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ} Q) ∨
     ([†κ] ∗ |={E∖↑lftN,E}=> True).
 Proof.
   iIntros (?) "#LFT HP".
@@ -76,7 +76,7 @@ Qed.
 Lemma bor_acc_cons E q κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗
-    ∀ Q, ▷ (▷ Q ={↑lft_userN}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ} Q ∗ q.[κ].
+    ∀ Q, ▷ (▷ Q ={userE}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ} Q ∗ q.[κ].
 Proof.
   iIntros (?) "#LFT HP Htok".
   iMod (bor_acc_strong with "LFT HP Htok") as (κ') "(#Hκκ' & $ & Hclose)"; first done.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index bc2c943b1788532e7f8ad626f07c442ac4929f19..908cc2e3fb5cfb3319b5c50c19c6f49ce03515d5 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -6,15 +6,14 @@ From iris.bi Require Import fractional.
 Set Default Proof Using "Type".
 
 Definition lftN : namespace := nroot .@ "lft".
-(** A (disjoint) mask that is available in the "consequence" view shift of
-    borrow accessors. *)
-Definition lft_userN : namespace := nroot .@ "lft_usr".
 
 Module Type lifetime_sig.
   (** CMRAs needed by the lifetime logic  *)
   (* We can't instantie the module parameters with inductive types, so we
      have aliases here. *)
-  Parameter lftG' : gFunctors → Set.
+  (** userE is a (disjoint) mask that is available in the "consequence" view
+      shift of borrow accessors. *)
+  Parameter lftG' : ∀ (Σ : gFunctors) (userE : coPset), Set.
   Global Notation lftG := lftG'.
   Existing Class lftG'.
   Parameter lftPreG' : gFunctors → Set.
@@ -26,17 +25,17 @@ Module Type lifetime_sig.
   Parameter static : lft.
   Declare Instance lft_intersect : Meet lft.
 
-  Parameter lft_ctx : ∀ `{!invG Σ, !lftG Σ}, iProp Σ.
+  Parameter lft_ctx : ∀ `{!invG Σ, !lftG Σ userE}, iProp Σ.
 
-  Parameter lft_tok : ∀ `{!lftG Σ} (q : Qp) (κ : lft), iProp Σ.
-  Parameter lft_dead : ∀ `{!lftG Σ} (κ : lft), iProp Σ.
+  Parameter lft_tok : ∀ `{!lftG Σ userE} (q : Qp) (κ : lft), iProp Σ.
+  Parameter lft_dead : ∀ `{!lftG Σ userE} (κ : lft), iProp Σ.
 
-  Parameter lft_incl : ∀ `{!invG Σ, !lftG Σ} (κ κ' : lft), iProp Σ.
-  Parameter bor : ∀ `{!invG Σ, !lftG Σ} (κ : lft) (P : iProp Σ), iProp Σ.
+  Parameter lft_incl : ∀ `{!invG Σ, !lftG Σ userE} (κ κ' : lft), iProp Σ.
+  Parameter bor : ∀ `{!invG Σ, !lftG Σ userE} (κ : lft) (P : iProp Σ), iProp Σ.
 
   Parameter bor_idx : Type.
-  Parameter idx_bor_own : ∀ `{!lftG Σ} (q : frac) (i : bor_idx), iProp Σ.
-  Parameter idx_bor : ∀ `{!invG Σ, !lftG Σ} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
+  Parameter idx_bor_own : ∀ `{!lftG Σ userE} (q : frac) (i : bor_idx), iProp Σ.
+  Parameter idx_bor : ∀ `{!invG Σ, !lftG Σ userE} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
 
   (** Our lifetime creation lemma offers allocating a lifetime that is defined
   by a [positive] in some given infinite set. This operation converts the
@@ -54,7 +53,7 @@ Module Type lifetime_sig.
   Infix "⊑" := lft_incl (at level 70) : bi_scope.
 
   Section properties.
-  Context `{!invG Σ, !lftG Σ}.
+  Context `{!invG Σ, !lftG Σ userE}.
 
   (** * Instances *)
   Global Declare Instance lft_inhabited : Inhabited lft.
@@ -109,7 +108,7 @@ Module Type lifetime_sig.
   Parameter lft_create_strong : ∀ P E, pred_infinite P → ↑lftN ⊆ E →
     lft_ctx ={E}=∗
     ∃ p : positive, let κ := positive_to_lft p in ⌜P p⌝ ∗
-         (1).[κ] ∗ □ ((1).[κ] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†κ]).
+         (1).[κ] ∗ □ ((1).[κ] ={↑lftN ∪ userE}[userE]▷=∗ [†κ]).
   Parameter bor_create : ∀ E κ P,
     ↑lftN ⊆ E → lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
   Parameter bor_fake : ∀ E κ P,
@@ -143,11 +142,11 @@ Module Type lifetime_sig.
      shift, we cannot turn [†κ'] into [†κ]. *)
   Parameter bor_acc_strong : ∀ E q κ P, ↑lftN ⊆ E →
     lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ∃ κ', κ ⊑ κ' ∗ ▷ P ∗
-      ∀ Q, ▷ (▷ Q -∗ [†κ'] ={↑lft_userN}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ'} Q ∗ q.[κ].
+      ∀ Q, ▷ (▷ Q -∗ [†κ'] ={userE}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ'} Q ∗ q.[κ].
   Parameter bor_acc_atomic_strong : ∀ E κ P, ↑lftN ⊆ E →
     lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
       (∃ κ', κ ⊑ κ' ∗ ▷ P ∗
-         ∀ Q, ▷ (▷ Q -∗ [†κ'] ={↑lft_userN}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
+         ∀ Q, ▷ (▷ Q -∗ [†κ'] ={userE}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
            ([†κ] ∗ |={E∖↑lftN,E}=> True).
 
   (* Because Coq's module system is horrible, we have to repeat properties of lft_incl here
@@ -173,6 +172,7 @@ Module Type lifetime_sig.
   Parameter lftΣ : gFunctors.
   Global Declare Instance subG_lftPreG Σ : subG lftΣ Σ → lftPreG Σ.
 
-  Parameter lft_init : ∀ `{!invG Σ, !lftPreG Σ} E, ↑lftN ⊆ E →
-    ⊢ |={E}=> ∃ _ : lftG Σ, lft_ctx.
+  Parameter lft_init : ∀ `{!invG Σ, !lftPreG Σ} E userE,
+    ↑lftN ⊆ E → ↑lftN ## userE →
+    ⊢ |={E}=> ∃ _ : lftG Σ userE, lft_ctx.
 End lifetime_sig.
diff --git a/theories/lifetime/meta.v b/theories/lifetime/meta.v
index 39e6907dd5c80459d6cabf8fad4a6d4be7215c78..d0f911ba82ca0af00a2826c5d5feae500143c587 100644
--- a/theories/lifetime/meta.v
+++ b/theories/lifetime/meta.v
@@ -21,12 +21,12 @@ we need. In other words, we use [own_unit] instead of [own_alloc]. As a result
 we can just hard-code an arbitrary name here. *)
 Local Definition lft_meta_gname : gname := 42%positive.
 
-Definition lft_meta `{!lftG Σ, lft_metaG Σ} (κ : lft) (γ : gname) : iProp Σ :=
+Definition lft_meta `{!lftG Σ userE, lft_metaG Σ} (κ : lft) (γ : gname) : iProp Σ :=
   ∃ p : positive, ⌜κ = positive_to_lft p⌝ ∗
     own lft_meta_gname (dyn_reservation_map_data p (to_agree γ)).
 
 Section lft_meta.
-  Context `{!invG Σ, !lftG Σ, lft_metaG Σ}.
+  Context `{!invG Σ, !lftG Σ userE, lft_metaG Σ}.
 
   Global Instance lft_meta_timeless κ γ : Timeless (lft_meta κ γ).
   Proof. apply _. Qed.
@@ -36,7 +36,7 @@ Section lft_meta.
   Lemma lft_create_meta {E : coPset} (γ : gname) :
     ↑lftN ⊆ E →
     lft_ctx ={E}=∗
-    ∃ κ, lft_meta κ γ ∗ (1).[κ] ∗ □ ((1).[κ] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†κ]).
+    ∃ κ, lft_meta κ γ ∗ (1).[κ] ∗ □ ((1).[κ] ={↑lftN ∪ userE}[userE]▷=∗ [†κ]).
   Proof.
     iIntros (HE) "#LFT".
     iMod (own_unit (dyn_reservation_mapUR (agreeR gnameO)) lft_meta_gname) as "Hown".
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 913c8dd0f134a79af8801ac4031a83fda6399afd..a905436199c911a64f3de54b9547ef790af3360c 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -5,7 +5,7 @@ From iris.base_logic.lib Require Import boxes.
 Set Default Proof Using "Type".
 
 Section accessors.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invG Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 (* Helper internal lemmas *)
@@ -55,7 +55,7 @@ Proof.
 Qed.
 
 Lemma add_vs Pb Pb' P Q Pi κ :
-  ▷ (Pb ≡ (P ∗ Pb')) -∗ lft_vs κ Pb Pi -∗ (▷ Q -∗ [†κ] ={↑lft_userN}=∗ ▷ P) -∗
+  ▷ (Pb ≡ (P ∗ Pb')) -∗ lft_vs κ Pb Pi -∗ (▷ Q -∗ [†κ] ={userE}=∗ ▷ P) -∗
   lft_vs κ (Q ∗ Pb') Pi.
 Proof.
   iIntros "#HEQ Hvs HvsQ". iApply (lft_vs_cons with "[-Hvs] Hvs").
@@ -148,7 +148,7 @@ Qed.
 Lemma bor_acc_strong E q κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ∃ κ', κ ⊑ κ' ∗ ▷ P ∗
-    ∀ Q, ▷(▷ Q -∗ [†κ'] ={↑lft_userN}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ'} Q ∗ q.[κ].
+    ∀ Q, ▷(▷ Q -∗ [†κ'] ={userE}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ'} Q ∗ q.[κ].
 Proof.
   unfold bor, raw_bor. iIntros (HE) "#LFT Hbor Htok".
   iDestruct "Hbor" as (κ'') "(#Hle & Htmp)". iDestruct "Htmp" as (s'') "(Hbor & #Hs)".
@@ -215,7 +215,7 @@ Lemma bor_acc_atomic_strong E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
    (∃ κ', κ ⊑ κ' ∗ ▷ P ∗
-      ∀ Q, ▷ (▷ Q -∗ [†κ'] ={↑lft_userN}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
+      ∀ Q, ▷ (▷ Q -∗ [†κ'] ={userE}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
     ([†κ] ∗ |={E∖↑lftN,E}=> True).
 Proof.
   iIntros (HE) "#LFT Hbor". rewrite bor_unfold_idx /idx_bor /bor /raw_bor.
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 03ff321de45284ee6170d7c1f25ceb01f33b93e7..4ac85ae95053f5fcd6ab1d3ca0051ca53a45152b 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section borrow.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invG Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 Lemma raw_bor_create E κ P :
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 3a4348e8339d3018f178b3d7bf39f9090bdadd9c..21d8c87bb04eff13dcff110f1844d22dc2a5a26e 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section borrow.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invG Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 Lemma bor_sep E κ P Q :
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 8d0a45bfa4b2281df3df82e1f598c129933ca678..df1f6d4c69c7b4c166d53cd3a37fe7ebf57f7c11 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section creation.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invG Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
@@ -16,7 +16,7 @@ Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
     ([∗ set] κ' ∈ K', lft_inv_alive κ'))%I in
   (∀ κ', is_Some (I !! κ') → κ ⊂ κ' → κ' ∈ K) →
   (∀ κ', is_Some (I !! κ') → κ' ⊂ κ → κ' ∈ K') →
-  Iinv -∗ lft_inv_alive κ -∗ [†κ] ={↑lft_userN ∪ ↑borN ∪ ↑inhN}=∗ Iinv ∗ lft_inv_dead κ.
+  Iinv -∗ lft_inv_alive κ -∗ [†κ] ={userE ∪ ↑borN ∪ ↑inhN}=∗ Iinv ∗ lft_inv_dead κ.
 Proof.
   iIntros (Iinv HK HK') "(HI & Hdead & Halive) Hlalive Hκ".
   rewrite lft_inv_alive_unfold;
@@ -63,7 +63,7 @@ Lemma lfts_kill (A : gmap atomic_lft _) (I : gmap lft lft_names) (K K' : gset lf
   (∀ κ κ', κ ∈ K → is_Some (I !! κ') → κ ⊆ κ' → κ' ∈ K) →
   (∀ κ, lft_alive_in A κ → is_Some (I !! κ) → κ ∉ K → κ ∈ K') →
   Iinv K' -∗ ([∗ set] κ ∈ K, lft_inv A κ ∗ [†κ])
-    ={↑lft_userN ∪ ↑borN ∪ ↑inhN}=∗ Iinv K' ∗ [∗ set] κ ∈ K, lft_inv_dead κ.
+    ={userE ∪ ↑borN ∪ ↑inhN}=∗ Iinv K' ∗ [∗ set] κ ∈ K, lft_inv_dead κ.
 Proof.
   intros Iinv. revert K'.
   induction (set_wf K) as [K _ IH]=> K' HKK' HK HK'.
@@ -112,9 +112,9 @@ Lemma lft_create_strong P E :
   pred_infinite P → ↑lftN ⊆ E →
   lft_ctx ={E}=∗
   ∃ p : positive, let κ := positive_to_lft p in ⌜P p⌝ ∗
-       (1).[κ] ∗ □ ((1).[κ] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†κ]).
+       (1).[κ] ∗ □ ((1).[κ] ={↑lftN ∪ userE}[userE]▷=∗ [†κ]).
 Proof.
-  iIntros (HP ?) "#LFT".
+  assert (userE_lftN_disj:=userE_lftN_disj). iIntros (HP ?) "#LFT".
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
   rewrite ->pred_infinite_set in HP.
   destruct (HP (dom (gset _) A)) as [Λ [HPx HΛ%not_elem_of_dom]].
@@ -131,10 +131,9 @@ Proof.
   iModIntro; iExists Λ.
   rewrite {1}/lft_tok big_sepMS_singleton. iSplit; first done. iFrame "HΛ".
   clear I A HΛ. iIntros "!> HΛ".
-  iApply (step_fupd_mask_mono (↑lftN ∪ ↑lft_userN) _ ((↑lftN ∪ ↑lft_userN)∖↑mgmtN)).
+  iApply (step_fupd_mask_mono (↑lftN ∪ userE) _ ((↑lftN ∪ userE)∖↑mgmtN)).
   { (* FIXME solve_ndisj should really handle this... *)
-    assert (↑lft_userN ## ↑mgmtN) by solve_ndisj.
-    set_solver. }
+    assert (↑mgmtN ## userE) by solve_ndisj. set_solver. }
   { done. }
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
   { (* FIXME solve_ndisj should really handle this... *)
@@ -160,10 +159,10 @@ Proof.
   { iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!>".
     iIntros (κ [? _]%elem_of_kill_set) "$". rewrite /lft_dead. eauto. }
   iApply fupd_trans.
-  iApply (fupd_mask_mono (↑lft_userN ∪ ↑borN ∪ ↑inhN)).
+  iApply (fupd_mask_mono (userE ∪ ↑borN ∪ ↑inhN)).
   { (* FIXME can we make solve_ndisj handle this? *)
-    clear. rewrite -assoc. apply union_least.
-    - assert (↑lft_userN ##@{coPset} ↑mgmtN) by solve_ndisj. set_solver.
+    clear -userE_lftN_disj. rewrite -assoc. apply union_least.
+    - assert (userE ##@{coPset} ↑mgmtN) by solve_ndisj. set_solver.
     - assert (↑inhN ##@{coPset} ↑mgmtN) by solve_ndisj.
       assert (↑inhN ⊆@{coPset} ↑lftN) by solve_ndisj.
       assert (↑borN ##@{coPset} ↑mgmtN) by solve_ndisj.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index b4556a06603292f67377da5934c14ca9c87f79c7..5fdd5dcd560eb4367e0ff1b59b8ddeda3ea2bc55 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -40,7 +40,7 @@ Definition ilftUR := gmapUR lft (agreeR lft_namesO).
 Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateO)).
 Definition inhUR := gset_disjUR slice_name.
 
-Class lftG Σ := LftG {
+Class lftG Σ (userE : coPset) := LftG {
   lft_box :> boxG Σ;
   alft_inG :> inG Σ (authR alftUR);
   alft_name : gname;
@@ -49,6 +49,7 @@ Class lftG Σ := LftG {
   lft_bor_inG :> inG Σ (authR borUR);
   lft_cnt_inG :> inG Σ (authR natUR);
   lft_inh_inG :> inG Σ (authR inhUR);
+  userE_lftN_disj : ↑lftN ## userE;
 }.
 Definition lftG' := lftG.
 
@@ -79,7 +80,7 @@ Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap to_agree.
 Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,.) ∘ to_agree).
 
 Section defs.
-  Context `{!invG Σ, !lftG Σ}.
+  Context `{!invG Σ, !lftG Σ userE}.
 
   Definition lft_tok (q : Qp) (κ : lft) : iProp Σ :=
     ([∗ mset] Λ ∈ κ, own alft_name (◯ {[ Λ := Cinl q ]}))%I.
@@ -142,7 +143,7 @@ Section defs.
        own_cnt κ (● n) ∗
        ∀ I : gmap lft lft_names,
          lft_vs_inv_go κ lft_inv_alive I -∗ ▷ Pb -∗ lft_dead κ
-           ={↑lft_userN ∪ ↑borN}=∗
+           ={userE ∪ ↑borN}=∗
          lft_vs_inv_go κ lft_inv_alive I ∗ ▷ Pi ∗ own_cnt κ (◯ n))%I.
 
   Definition lft_inv_alive_go (κ : lft)
@@ -223,7 +224,7 @@ Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
   idx_bor_own idx_bor raw_bor bor.
 
 Section basic_properties.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invG Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 (* Unfolding lemmas *)
@@ -270,7 +271,7 @@ Lemma lft_vs_unfold κ Pb Pi :
   lft_vs κ Pb Pi ⊣⊢ ∃ n : nat,
     own_cnt κ (● n) ∗
     ∀ I : gmap lft lft_names,
-      lft_vs_inv κ I -∗ ▷ Pb -∗ lft_dead κ ={↑lft_userN ∪ ↑borN}=∗
+      lft_vs_inv κ I -∗ ▷ Pb -∗ lft_dead κ ={userE ∪ ↑borN}=∗
       lft_vs_inv κ I ∗ ▷ Pi ∗ own_cnt κ (◯ n).
 Proof. done. Qed.
 
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 101ca0ee3fc30468c91df1668d0b2a62e4da1e99..793b7d74d9feb4f98c0f0d901a5af4e07b185bd6 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section faking.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invG Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 Lemma ilft_create A I κ :
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 043fb967ed8cab5866aa3111d4aec32d29bf2a66..a82d3fc4770bf6d24a026664618d76b686d91e43 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -6,8 +6,21 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
 
+Lemma lft_init `{!invG Σ, !lftPreG Σ} E userE :
+  ↑lftN ⊆ E → ↑lftN ## userE → ⊢ |={E}=> ∃ _ : lftG Σ userE, lft_ctx.
+Proof.
+  iIntros (? HuserE). rewrite /lft_ctx.
+  iMod (own_alloc (● ∅ : authR alftUR)) as (γa) "Ha"; first by apply auth_auth_valid.
+  iMod (own_alloc (● ∅ : authR ilftUR)) as (γi) "Hi"; first by apply auth_auth_valid.
+  set (HlftG := LftG _ _ _ _ γa _ γi _ _ _ HuserE). iExists HlftG.
+  iMod (inv_alloc _ _ lfts_inv with "[Ha Hi]") as "$"; last done.
+  iModIntro. rewrite /lfts_inv /own_alft_auth /own_ilft_auth. iExists ∅, ∅.
+  rewrite /to_alftUR /to_ilftUR !fmap_empty. iFrame.
+  rewrite dom_empty_L big_sepS_empty. done.
+Qed.
+
 Section primitive.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invG Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 Lemma to_borUR_included (B : gmap slice_name bor_state) i s q :
@@ -18,19 +31,6 @@ Proof.
   by move=> /Some_pair_included [_] /Some_included_total /to_agree_included=>->.
 Qed.
 
-Lemma lft_init `{!lftPreG Σ} E :
-  ↑lftN ⊆ E → ⊢ |={E}=> ∃ _ : lftG Σ, lft_ctx.
-Proof.
-  iIntros (?). rewrite /lft_ctx.
-  iMod (own_alloc (● ∅ : authR alftUR)) as (γa) "Ha"; first by apply auth_auth_valid.
-  iMod (own_alloc (● ∅ : authR ilftUR)) as (γi) "Hi"; first by apply auth_auth_valid.
-  set (HlftG := LftG _ _ _ γa _ γi _ _ _). iExists HlftG.
-  iMod (inv_alloc _ _ lfts_inv with "[Ha Hi]") as "$"; last done.
-  iModIntro. rewrite /lfts_inv /own_alft_auth /own_ilft_auth. iExists ∅, ∅.
-  rewrite /to_alftUR /to_ilftUR !fmap_empty. iFrame.
-  rewrite dom_empty_L big_sepS_empty. done.
-Qed.
-
 (** Ownership *)
 Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
   own_ilft_auth I -∗
@@ -497,7 +497,7 @@ Proof.
 Qed.
 
 Lemma lft_vs_cons κ Pb Pb' Pi :
-  (▷ Pb'-∗ [†κ] ={↑lft_userN ∪ ↑borN}=∗ ▷ Pb) -∗
+  (▷ Pb'-∗ [†κ] ={userE ∪ ↑borN}=∗ ▷ Pb) -∗
   lft_vs κ Pb Pi -∗ lft_vs κ Pb' Pi.
 Proof.
   iIntros "Hcons Hvs". rewrite !lft_vs_unfold.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 721a53a4f786185d85007a095779d376df988412..27ee3e79b5184d040f895be01e894a553db966a2 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section reborrow.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invG Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 (* Notice that taking lft_inv for both κ and κ' already implies
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 81816c747f5f537d9e670735dc01817679787b24..fa964406411cbde05f390652141b692c40617883 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -3,7 +3,7 @@ From iris.base_logic.lib Require Export na_invariants.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
-Definition na_bor `{!invG Σ, !lftG Σ, !na_invG Σ}
+Definition na_bor `{!invG Σ, !lftG Σ userE, !na_invG Σ}
            (κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own 1 i))%I.
 
@@ -11,7 +11,7 @@ Notation "&na{ κ , tid , N }" := (na_bor κ tid N)
     (format "&na{ κ , tid , N }") : bi_scope.
 
 Section na_bor.
-  Context `{!invG Σ, !lftG Σ, !na_invG Σ}
+  Context `{!invG Σ, !lftG Σ userE, !na_invG Σ}
           (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ).
 
   Global Instance na_bor_ne κ n : Proper (dist n ==> dist n) (na_bor κ tid N).
diff --git a/theories/typing/base.v b/theories/typing/base.v
index 3ccbee1fc01fcf598cacb107645605c8ee40ed7b..e5a84f36cae932f533ca82659afa1d08a95b3a95 100644
--- a/theories/typing/base.v
+++ b/theories/typing/base.v
@@ -1,3 +1,4 @@
+From stdpp Require Import namespaces.
 From lrust.lang Require Export proofmode.
 
 (* Last, so that we make sure we shadow the defintion of delete for
@@ -6,6 +7,19 @@ From lrust.lang.lib Require Export new_delete.
 
 Open Scope Z_scope.
 
+Definition lft_userN : namespace := nroot .@ "lft_usr".
+
+(* The "user mask" of the lifetime logic. This needs to be disjoint with ↑lftN.
+
+   If a client library desires to put invariants in lft_userE, then it is
+   encouraged to place it in the already defined lft_userN. On the other hand,
+   extensions to the model of RustBelt itself (such as gpfsl for
+   the weak-mem extension) can require extending [lft_userE] with the relevant
+   namespaces. In that case all client libraries need to be re-checked to
+   ensure disjointness of [lft_userE] with their masks is maintained where
+   necessary. *)
+Definition lft_userE : coPset := ↑lft_userN.
+
 Create HintDb lrust_typing.
 Create HintDb lrust_typing_merge.
 
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 265c642b3d342cf227a367da32ab60df876f8055..3f3c144a7e3512ab48f342a1f4cd98e7515f07c7 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -23,7 +23,7 @@ Notation llctx := (list llctx_elt).
 Notation "κ ⊑ₗ κl" := (@pair lft (list lft) κ κl) (at level 70).
 
 Section lft_contexts.
-  Context `{!invG Σ, !lftG Σ}.
+  Context `{!invG Σ, !lftG Σ lft_userE}.
   Implicit Type (κ : lft).
 
   (* External lifetime contexts. *)
@@ -52,7 +52,7 @@ Section lft_contexts.
     std++ we use here does not yet have [min] on [Qp].
     We do the cap so that we never need to have more than [1] of this token. *)
     let qeff := (if decide (1 ≤ qmax) then 1 else qmax)%Qp in
-    (∃ κ0, ⌜x.1 = κ' ⊓ κ0⌝ ∗ qeff.[κ0] ∗ (qeff.[κ0] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†κ0]))%I.
+    (∃ κ0, ⌜x.1 = κ' ⊓ κ0⌝ ∗ qeff.[κ0] ∗ (qeff.[κ0] ={↑lftN ∪ lft_userE}[lft_userE]▷=∗ [†κ0]))%I.
   (* Local lifetime contexts without the "ending a lifetime" viewshifts -- these
   are fractional. *)
   Definition llctx_elt_interp_noend (qmax : Qp) (x : llctx_elt) (q : Qp) : iProp Σ :=
@@ -415,7 +415,7 @@ Arguments lctx_lft_incl_incl_noend {_ _ _ _} _ _.
 Arguments lctx_lft_alive_tok {_ _ _ _ _} _ _ _.
 Arguments lctx_lft_alive_tok_noend {_ _ _ _ _} _ _ _.
 
-Lemma elctx_sat_submseteq `{!invG Σ, !lftG Σ} E E' L :
+Lemma elctx_sat_submseteq `{!invG Σ, !lftG Σ lft_userE} E E' L :
   E' ⊆+ E → elctx_sat E L E'.
 Proof. iIntros (HE' ??) "_ !> H". by iApply big_sepL_submseteq. Qed.
 
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 56ed0432524d70a176ae66629fcb0b5a16321e17..238dd508fb7872f26256cec465fd8933ebe27df1 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -26,7 +26,7 @@ Section arc.
      (*    because [weak_new] cannot prove ty_shr, even for a dead *)
      (*    lifetime. *)
      (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
-     □ (1.[ν] ={↑lftN ∪ ↑lft_userN ∪ ↑arc_endN}[↑lft_userN]▷=∗
+     □ (1.[ν] ={↑lftN ∪ lft_userE ∪ ↑arc_endN}[lft_userE]▷=∗
           [†ν] ∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ † l…(2 + ty.(ty_size))))%I.
 
   Global Instance arc_persist_ne tid ν γ l n :
@@ -86,9 +86,9 @@ Section arc.
       first by iRight; iApply "H". iIntros "!> !> Hν".
     iMod (inv_acc with "INV") as "[[H†|[$ Hvs]] Hclose]";
       [set_solver|iDestruct (lft_tok_dead with "Hν H†") as ">[]"|].
-    rewrite difference_union_distr_l_L difference_diag_L right_id_L
+    rewrite difference_union_distr_l_L difference_diag_L (right_id_L ∅)
             difference_disjoint_L; last first.
-    { apply disjoint_union_l. split; solve_ndisj. }
+    { apply disjoint_union_l; solve_ndisj. }
     iMod ("Hν†" with "Hν") as "H". iModIntro. iNext. iApply fupd_trans.
     iMod "H" as "#Hν".
     iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hvs" with "Hν") as "$".
diff --git a/theories/typing/lib/ghostcell.v b/theories/typing/lib/ghostcell.v
index 07242d83898de629041ff57bf43e4e00157da4d7..3aad5bf33c3b568403734836c84d9cad1c51b31b 100644
--- a/theories/typing/lib/ghostcell.v
+++ b/theories/typing/lib/ghostcell.v
@@ -393,7 +393,7 @@ Section ghostcell.
       by iFrame "Hidx Hown".
     + iIntros (r) "Hna Hf Hown".
       simpl_subst.
-      iDestruct ("Hcloseα" with "[Hf]") as "[Htok Hf]"; first by rewrite right_id.
+      iDestruct ("Hcloseα" with "[Hf]") as "[Htok Hf]"; [by rewrite (right_id static)|].
       iMod ("Hclosef" with "Hf HL") as "HL".
       wp_let.
       iApply (type_type _ _ _ [ r ◁ box R_F ] with "[] LFT HE Hna HL Hc"); try solve_typing;
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 84266a6d561488238c6678760d0a11e50e1eef9b..10251242c7f592d4226ff923c5fa9f8b9d929abd 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -84,7 +84,7 @@ Section rc.
                  because [weak_new] cannot prove ty_shr, even for a dead
                  lifetime. *)
               (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
-              □ (1.[ν] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†ν]))%I.
+              □ (1.[ν] ={↑lftN ∪ lft_userE}[lft_userE]▷=∗ [†ν]))%I.
 
   Global Instance rc_persist_persistent tid ν γ l ty : Persistent (rc_persist tid ν γ l ty).
   Proof. unfold rc_persist, tc_opaque. apply _. Qed.
@@ -246,16 +246,16 @@ Section code.
         (((⌜strong = 1%positive⌝ ∗
            (∃ weak : Z, (l +ₗ 1) ↦ #weak ∗
              ((⌜weak = 1⌝ ∗
-               |={⊤}[↑lft_userN]▷=> † l…(2 + ty.(ty_size)) ∗
+               |={⊤}[lft_userE]▷=> † l…(2 + ty.(ty_size)) ∗
                           ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ na_own tid F) ∨
              (⌜weak > 1⌝ ∗
               ((l ↦ #1 -∗ (l +ₗ 1) ↦ #weak
                 ={⊤}=∗ na_own tid F ∗ ty_own (rc ty) tid [ #l ]) ∧
                (l ↦ #0 -∗ (l +ₗ 1) ↦ #(weak - 1)
-                ={⊤}[↑lft_userN]▷=∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗
+                ={⊤}[lft_userE]▷=∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗
                 ((l +ₗ 2) ↦∗: (λ vl, ⌜length vl = ty.(ty_size)⌝)
                  ={⊤}=∗ na_own tid F)))))) ∧
-           (l ↦ #0 ={⊤}[↑lft_userN]▷=∗
+           (l ↦ #0 ={⊤}[lft_userE]▷=∗
              ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ † l…(2 + ty.(ty_size)) ∗ na_own tid F ∗
              (na_own tid F ={⊤}=∗ ∃ weak : Z,
                 (l +ₗ 1) ↦ #weak ∗
@@ -294,7 +294,7 @@ Section code.
              iMod (own_update_2 with "Hst Htok") as "Hst".
              { apply auth_update_dealloc. rewrite -{1}(right_id (None, 0%nat) _ (_, _)).
                apply cancel_local_update_unit, _. }
-             rewrite -[in (1).[ν]%I]Hqq' -[(|={↑lft_userN,⊤}=>_)%I]fupd_trans.
+             rewrite -[in (1).[ν]%I]Hqq' -[(|={lft_userE,⊤}=>_)%I]fupd_trans.
              iApply step_fupd_mask_mono;
                last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
              iModIntro. iNext. iMod "H†".
@@ -309,7 +309,7 @@ Section code.
                 iMod ("Hclose" with "[-Htok Hν1]") as "$"; last by auto 10 with iFrame.
                 iFrame. iExists _. auto with iFrame.
              ++ iIntros "Hl1 Hl2".
-                rewrite -[in (1).[ν]%I]Hqq' -[(|={↑lft_userN,⊤}=>_)%I]fupd_trans.
+                rewrite -[in (1).[ν]%I]Hqq' -[(|={lft_userE,⊤}=>_)%I]fupd_trans.
                 iApply step_fupd_mask_mono;
                   last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
                 iModIntro. iNext. iMod "H†".
@@ -330,7 +330,7 @@ Section code.
           { apply auth_update. etrans.
             - rewrite [(Some _, weak)]pair_split. apply cancel_local_update_unit, _.
             - apply (op_local_update _ _ (Some (Cinr (Excl tt)), 0%nat)). auto. }
-          rewrite -[(|={↑lft_userN,⊤}=>_)%I]fupd_trans -[in (1).[ν]%I]Hqq'.
+          rewrite -[(|={lft_userE,⊤}=>_)%I]fupd_trans -[in (1).[ν]%I]Hqq'.
           iApply step_fupd_mask_mono;
             last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
           iModIntro. iNext. iMod "H†".
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index ab9fce4c6fd3b7168ba10d8b10ba8f8d502488b4..9e16fc4f5043d53925d0631d433142e778b64070 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -14,7 +14,7 @@ Section ref_functions.
     own γ (◯ reading_stR q ν) -∗
     ∃ (q' : Qp) n, l ↦ #(Zpos n) ∗ ⌜(q ≤ q')%Qp⌝ ∗
             own γ (● (refcell_st_to_R $ Some (ν, false, q', n)) ⋅ ◯ reading_stR q ν) ∗
-            ((1).[ν] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗
+            ((1).[ν] ={↑lftN ∪ lft_userE}[lft_userE]▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗
             (∃ q'', ⌜(q' + q'' = 1)%Qp⌝ ∗ q''.[ν]) ∗
             ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1).
   Proof.
@@ -161,7 +161,7 @@ Section ref_functions.
       as (q' n) "(H↦lrc & >% & H●◯ & H† & Hq' & Hshr)".
     iDestruct "Hq'" as (q'') ">[% Hν']".
     wp_read. wp_let. wp_op. wp_write.
-    iAssert (|={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=> refcell_inv tid lrc γ β ty')%I
+    iAssert (|={↑lftN ∪ lft_userE}[lft_userE]▷=> refcell_inv tid lrc γ β ty')%I
       with "[H↦lrc H●◯ Hν Hν' Hshr H†]" as "INV".
     { iDestruct (own_valid with "H●◯") as
           %[[[[_ ?]?]|[[_ [q0 Hq0]]%prod_included [n' Hn']]%prod_included]
@@ -181,7 +181,7 @@ Section ref_functions.
           apply (cancel_local_update_unit (reading_stR q ν)), _. }
         iApply step_fupd_intro; first set_solver-. iExists (q+q'')%Qp. iFrame.
         by rewrite assoc (comm _ q0 q). }
-    wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN ∪ ↑lft_userN)); first done.
+    wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN ∪ lft_userE)); 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α". iMod ("Hclose" with "Hα HL") as "HL".
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index c56f81a0279304dd78adcee2184eb5e8715351b0..3cb95d6b9b896c66f74cda8f77b52f7bb9f0a6bb 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -49,7 +49,7 @@ Section refcell_inv.
         (* Not borrowed. *)
         &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)
       | Some (ν, rw, q, _) =>
-        (1.[ν] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
+        (1.[ν] ={↑lftN ∪ lft_userE}[lft_userE]▷=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
         (∃ q', ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν]) ∗
         if rw then (* Mutably borrowed. *) True
         else       (* Immutably borrowed. *) ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1)
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 3b721072a328c13ee9353dec6f862f1b48a5a301..f2f279ec3440f67854a8f73d7e06d80f34d0c816 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -193,7 +193,7 @@ Section refcell_functions.
         - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
           iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
             auth_update_alloc, (op_local_update_discrete _ _ (reading_stR (1/2)%Qp ν)).
-          rewrite right_id. iExists _, _. iFrame "Htok1 Hreading".
+          rewrite (right_id None). iExists _, _. iFrame "Htok1 Hreading".
           iDestruct (lft_intersect_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
           iApply (fupd_mask_mono (↑lftN)); first done.
           iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hst") as "[Hst Hh]". done.
@@ -276,7 +276,7 @@ Section refcell_functions.
       iMod (own_update with "Hownst") as "[Hownst ?]".
       { by eapply auth_update_alloc,
           (op_local_update_discrete _ _ (refcell_st_to_R $ Some (ν, true, (1/2)%Qp, xH))). }
-      rewrite right_id.
+      rewrite (right_id None).
       iApply fupd_wp. iApply (fupd_mask_mono (↑lftN)); first done.
       iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hb") as "[Hb Hbh]". done.
       { iApply lft_intersect_incl_l. }
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 4dfdcf69852acb3c13b15480282f1b906c0fe164..4b1c9d04f0f2a1ee34bd11bd136d60dd983e1d19 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -127,7 +127,7 @@ Section refmut_functions.
     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_read. wp_let. wp_op. wp_write.
-    iAssert (|={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=> refcell_inv tid lrc γ β ty')%I
+    iAssert (|={↑lftN ∪ lft_userE}[lft_userE]▷=> refcell_inv tid lrc γ β ty')%I
       with "[H↦lrc H● H◯ Hν INV]" as "INV".
     { iDestruct (own_valid_2 with "H● H◯") as
         %[[[=]|(? & [[? q'] ?] & [= <-] & Hst & INCL)]%option_included _]
@@ -152,7 +152,7 @@ Section refmut_functions.
         iApply step_fupd_intro; [set_solver-|]. iSplitL; [|done].
         iDestruct "Hq" as (q' ?) "?". iExists (q+q')%Qp. iFrame.
         rewrite assoc (comm _ q'' q) //. }
-    wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN ∪ ↑lft_userN)); first done.
+    wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN ∪ lft_userE)); first done.
     iApply (wp_step_fupd with "INV"); [set_solver-|]. wp_seq. iIntros "{Hb} Hb !>".
     iMod ("Hcloseβ" with "Hb Hna") as "[Hβ Hna]".
     iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL". wp_seq.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 414c865197d044fb4a48af95b9511b7016554797..e658e08d1b4bbee7c2f733be0fe9e53387bb0c81 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -40,7 +40,7 @@ Section rwlock_inv.
       | Some (Cinr (agν, q, n)) =>
         (* Locked for read. *)
         ∃ (ν : lft) q', agν ≡ to_agree ν ∗
-                □ (1.[ν] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†ν]) ∗
+                □ (1.[ν] ={↑lftN ∪ lft_userE}[lft_userE]▷=∗ [†ν]) ∗
                 ([†ν] ={↑lftN}=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid_own)) ∗
                 ty.(ty_shr) (α ⊓ ν) tid_shr (l +ₗ 1) ∗
                 ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν]
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 0582ee3b27aa3f1d180e74fcfbc97363a8c5c3ed..0a86013d747ea809a14973b5864ad96aec465559 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -182,7 +182,7 @@ Section rwlock_functions.
         iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
                          ty_shr ty (β ⊓ ν) tid (lx +ₗ 1) ∗
                          own γ (◯ reading_st qν ν) ∗ rwlock_inv tid tid lx γ β ty ∗
-                         ((1).[ν] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†ν]))%I
+                         ((1).[ν] ={↑lftN ∪ lft_userE}[lft_userE]▷=∗ [†ν]))%I
           with "[> Hlx Hownst Hst Hβtok2]"
           as (q' ν) "(Hβtok2 & Hν & Hshr & Hreading & INV & H†)".
         { destruct st' as [[|[[agν q] n]|]|]; try done.
@@ -202,7 +202,7 @@ Section rwlock_functions.
           - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". solve_ndisj.
             iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
               auth_update_alloc, (op_local_update_discrete _ _ (reading_st (1/2)%Qp ν)).
-            rewrite right_id. iExists _, _. iFrame "Htok1 Hreading".
+            rewrite (right_id None). iExists _, _. iFrame "Htok1 Hreading".
             iDestruct (lft_intersect_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
             iApply (fupd_mask_mono (↑lftN)). solve_ndisj.
             iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hst") as "[Hst Hh]". solve_ndisj.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index cb771c832c40eeade155046556faa3e968f754cd..d94c4ab85f4ae2e636ff14fba86c6ac65d89924f 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -23,7 +23,7 @@ Section rwlockreadguard.
            ∃ ν q γ β tid_own, ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
              α ⊑ β ∗ &at{β,rwlockN}(rwlock_inv tid_own tid l γ β ty) ∗
              q.[ν] ∗ own γ (◯ reading_st q ν) ∗
-             (1.[ν] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†ν])
+             (1.[ν] ={↑lftN ∪ lft_userE}[lft_userE]▷=∗ [†ν])
          | _ => False
          end;
        ty_shr κ tid l :=
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index d7d5245306da3ebae341cf3cbd745279b2e83801..f1d4d70e84df5f9840e295edf92d062bfa234741 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -83,7 +83,7 @@ Section rwlockreadguard_functions.
     iMod (at_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
     iDestruct "INV" as (st') "(Hlx & >H● & Hst)".
     destruct (decide (Z_of_rwlock_st st = Z_of_rwlock_st st')) as [->|?].
-    + iAssert (|={⊤ ∖ ↑rwlockN}[⊤ ∖ ↑rwlockN ∖ ↑lftN ∖ ↑lft_userN]▷=>
+    + iAssert (|={⊤ ∖ ↑rwlockN}[⊤ ∖ ↑rwlockN ∖ ↑lftN ∖ lft_userE]▷=>
                (lx' ↦ #(Z_of_rwlock_st st'-1) ==∗ rwlock_inv tid_own tid lx' γ β ty))%I
         with "[H● H◯ Hx' Hν Hst H†]" as "INV".
       { iDestruct (own_valid_2 with "H● H◯") as %[[[=]| (? & st0 & [=<-] & -> & [Heq|Hle])]
@@ -94,8 +94,8 @@ Section rwlockreadguard_functions.
           iDestruct "Hst" as (ν' q') "(>EQν & _ & Hh & _ & >Hq & >Hν')".
           rewrite -EQ. iDestruct "EQν" as %<-%(inj to_agree)%leibniz_equiv.
           iCombine "Hν" "Hν'" as "Hν". iDestruct "Hq" as %->.
-          iApply (step_fupd_mask_mono ((↑lftN ∪ ↑lft_userN) ∪ (⊤ ∖ ↑rwlockN ∖ ↑lftN ∖ ↑lft_userN)));
-            last iApply (step_fupd_mask_frame_r _ (↑lft_userN)).
+          iApply (step_fupd_mask_mono ((↑lftN ∪ lft_userE) ∪ (⊤ ∖ ↑rwlockN ∖ ↑lftN ∖ lft_userE)));
+            last iApply (step_fupd_mask_frame_r _ (lft_userE)).
           { set_solver-. }
           { solve_ndisj. }
           { rewrite difference_difference. apply: disjoint_difference_r1. done. }
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 1a5e14ff67cafa173ec02f69fb38a98b53d13825..4eba7c32762b73c276f8804491c6dabe8e342e7f 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -219,7 +219,7 @@ Section typing_rules.
     iIntros (Hc Hub) "He". iIntros (tid qmax) "#LFT #HE Htl [Hκ HL] HC HT".
     iDestruct "Hκ" as (Λ) "(% & Htok & Hend)".
     iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
-    iApply (wp_mask_mono _ (↑lftN ∪ ↑lft_userN)); first done.
+    iApply (wp_mask_mono _ (↑lftN ∪ lft_userE)); first done.
     iApply (wp_step_fupd with "Hend"); first set_solver-. wp_seq.
     iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT HE Htl HL HC [> -]").
     iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index c2cfca78955f5c319c53868f381fbb68730bd47e..4280bcf9f0a69584e8cdabd27207b17f80bf6c80 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -35,7 +35,7 @@ Section type_soundness.
     { split. by eapply adequate_nonracing.
       intros. by eapply (adequate_not_stuck _ (main [exit_cont]%E)). }
     apply: lrust_adequacy=>?. iIntros "_".
-    iMod lft_init as (?) "#LFT". done.
+    iMod (lft_init _ lft_userE) as (?) "#LFT"; [done|solve_ndisj|].
     iMod na_alloc as (tid) "Htl". set (Htype := TypeG _ _ _ _ _).
     wp_bind (of_val main). iApply (wp_wand with "[Htl]").
     iApply (Hmain Htype [] [] $! tid 1%Qp with "LFT [] Htl [] []").
diff --git a/theories/typing/type.v b/theories/typing/type.v
index a3d4977e61b9b56cbecf1d25b16f528a4e4d7084..09cb325cae62ce7f7bccdb2400b50db9e2e0432d 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -8,7 +8,7 @@ Set Default Proof Using "Type".
 
 Class typeG Σ := TypeG {
   type_lrustG :> lrustG Σ;
-  type_lftG :> lftG Σ;
+  type_lftG :> lftG Σ lft_userE;
   type_na_invG :> na_invG Σ;
   type_frac_borrowG :> frac_borG Σ
 }.