diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index 137f34050a09203623a58e088f1f2c16d429e9e5..a4f987f3a1a29e43641a56aaa63bb6c0adac2b3d 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -27,7 +27,7 @@ Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
 Proof. solve_inG. Qed.
 
 Section proof.
-  Context `{noprolG Σ, !lftG Σ view_Lat (↑histN), lockG Σ}.
+  Context `{noprolG Σ, !lftG Σ view_Lat lft_userE, lockG Σ}.
 
   Implicit Types (l : loc).
   Local Notation vProp := (vProp Σ).
@@ -84,7 +84,7 @@ Section proof.
 
   (** The main proofs. *)
   Lemma lock_proto_create N l q κ (R : vProp) E
-    (DISJ: N ## lftN) (SUB: ↑lftN ⊆ E):
+    (DISJ: N ## lftN) (SUB: ↑lftN ⊆ E) (histN_lft_userE : ↑histN ⊆ lft_userE):
     ⎡ lft_ctx ⎤ -∗ (q).[κ] -∗ ▷ ⎡ hist_inv ⎤ -∗
     &{κ}(∃ b: bool, l ↦ #b) -∗ ▷ R ={E}=∗
       (q).[κ] ∗ ∃ γ, lock_proto N l γ κ R.
@@ -97,7 +97,7 @@ Section proof.
        subst v. by iExists _. }
     { iDestruct "Hl" as (b) "Hl". iExists _. iFrame. by iExists _. }
     iMod (GPS_aPP_Init N (lock_interp R) l κ () q (λ v, ⌜∃ b : bool, v = #b⌝)%I
-          with "LFT Htok HINV Hl [R] []") as "[$ Hproto]"; [done|done|..].
+          with "LFT Htok HINV Hl [R] []") as "[$ Hproto]"; [done|done|done|..].
     { iIntros (t γ v) "#Eqb". iDestruct "Eqb" as (b) "Eqb". iExists b.
       iFrame "Eqb". by destruct b. }
     { iIntros "!>" (??? v). iDestruct 1 as (b) "[? ?]". by iExists _. }
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 7ac073086782b7a45fb7e034e714610c5565f516..f0b98b8a229500c43ce93f7530fbe70d06ec3303 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -58,7 +58,7 @@ Module Type lifetime_sig.
 
   (** * Notation *)
   Notation "q .[ κ ]" := (lft_tok q κ)
-      (format "q .[ κ ]", at level 0) : bi_scope.
+      (format "q .[ κ ]", at level 2, left associativity) : bi_scope.
   Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): bi_scope.
 
   Notation "&{ κ }" := (bor κ) (format "&{ κ }") : bi_scope.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index e9389716b2a0e8863679e33c262930d99806253b..0750228b59bc6b239ee19bde7b888ab52ea90781 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -180,8 +180,10 @@ Proof.
     iDestruct (monPred_in_intro True%I with "[//]") as (V) "[H _]".
     by rewrite -(lat_bottom_sqsubseteq V). }
   clear I A HΛ. iIntros "!> HΛ".
-  iApply (step_fupd_mask_mono (↑lftN ∪ userE) _ ((↑lftN ∪ userE)∖↑mgmtN)); [|done|].
-  { assert (↑mgmtN ## userE) by (pose proof userE_lftN_disj; solve_ndisj). set_solver. }
+  iApply (step_fupd_mask_mono (↑lftN ∪ userE) _ ((↑lftN ∪ userE)∖↑mgmtN)).
+  { (* FIXME solve_ndisj should really handle this... *)
+    assert (↑mgmtN ## userE) by solve_ndisj. set_solver. }
+  { done. }
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
   { rewrite <-union_subseteq_l. solve_ndisj. }
   iMod (ilft_create _ _ {[+ Λ +]} with "HA HI Hinv") as "H". clear A I.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index a27b1a154cb4761864a8c371011ea97446ed382c..31feccb7c60db67bbd9d0b0e0b6550c4132e71f0 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -220,7 +220,7 @@ Instance: Params (@raw_bor) 5 := {}.
 Instance bor_params : Params (@bor) 5 := {}.
 
 Notation "q .[ κ ]" := (lft_tok q κ)
-    (format "q .[ κ ]", at level 0) : bi_scope.
+    (format "q .[ κ ]", at level 2, left associativity) : bi_scope.
 Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): bi_scope.
 
 Notation "&{ κ }" := (bor κ) (format "&{ κ }") : bi_scope.
diff --git a/theories/logic/gps.v b/theories/logic/gps.v
index 114d6d1ca98f8cbc7ccab23673e3692df22a2890..0581f1c698276b8fcb5ba03994033cd0c3511dec 100644
--- a/theories/logic/gps.v
+++ b/theories/logic/gps.v
@@ -4,7 +4,7 @@ From lrust.lifetime Require Import at_borrow.
 From gpfsl.gps Require Import middleware.
 
 Section gps_at_bor_SP.
-Context `{!noprolG Σ, !gpsG Σ Prtcl, !lftG Σ view_Lat (↑histN)} (N: namespace).
+Context `{!noprolG Σ, !gpsG Σ Prtcl, !lftG Σ view_Lat lft_userE} (N: namespace).
 Local Notation vProp := (vProp Σ).
 
 Implicit Types (IP : interpO Σ Prtcl) (IPC: interpCasO Σ Prtcl) (l : loc)
@@ -21,11 +21,11 @@ Definition GPS_aSP_SharedWriter IP IPC l κ t s v γ : vProp :=
   (GPS_SWSharedWriter l t s v γ ∗ &at{κ, N} (GPS_INV IP l IPC γ))%I.
 
 Lemma GPS_aSP_Init IP IPC l κ s q P (Q: time → val → gname → vProp) E
-  (DISJ: N ## lftN) (SUB: ↑lftN ⊆ E):
+  (DISJ: N ## lftN) (SUB: ↑lftN ⊆ E) (histN_lft_userE : ↑histN ⊆ lft_userE):
   ⎡ lft_ctx ⎤ -∗ (q).[κ] -∗ ▷ ⎡ hist_inv ⎤ -∗
   &{κ} (∃ v, l ↦ v ∗ P v) -∗
   (∀ t γ v, ▷ P v -∗ GPS_SWWriter l t s v γ ={E}=∗ ▷ IP true l γ t s v ∗ Q t v γ) -∗
-  (□ ∀ t γ s v, ▷ IP true l γ t s v ={↑histN}=∗ ▷ P v) ={E}=∗
+  (□ ∀ t γ s v, ▷ IP true l γ t s v ={lft_userE}=∗ ▷ P v) ={E}=∗
   (q).[κ] ∗ ∃ γ t v, GPS_aSP_Reader IP IPC l κ t s v γ ∗ Q t v γ.
 Proof.
   iIntros "#LFT Htok #HINV Hl HP #HP2".
@@ -231,7 +231,7 @@ Qed.
 End gps_at_bor_SP.
 
 Section gps_at_bor_PP.
-Context `{!noprolG Σ, !gpsG Σ Prtcl, !gpsExAgG Σ, !lftG Σ view_Lat (↑histN)}
+Context `{!noprolG Σ, !gpsG Σ Prtcl, !gpsExAgG Σ, !lftG Σ view_Lat lft_userE}
         (N: namespace).
 Local Notation vProp := (vProp Σ).
 
@@ -250,11 +250,12 @@ Lemma GPS_aPP_lft_mono IP l κ κ' t s v γ :
   κ' ⊑ κ -∗ GPS_aPP IP l κ t s v γ -∗ GPS_aPP IP l κ' t s v γ.
 Proof. iIntros "#Hincl". iDestruct 1 as "[$ Inv]". by iApply at_bor_shorten. Qed.
 
-Lemma GPS_aPP_Init IP l κ s q P E (DISJ: N ## lftN) (SUB: ↑lftN ⊆ E):
+Lemma GPS_aPP_Init IP l κ s q P E (DISJ: N ## lftN) (SUB: ↑lftN ⊆ E)
+      (histN_lft_userE : ↑histN ⊆ lft_userE):
   ⎡ lft_ctx ⎤ -∗ (q).[κ] -∗ ▷ ⎡ hist_inv ⎤ -∗
   &{κ} (∃ v, l ↦ v ∗ P v) -∗
   (∀ t γ v, ▷ P v -∗ ▷ IP true l γ t s v) -∗
-  (□ ∀ t γ s v, ▷ IP true l γ t s v ={↑histN}=∗ ▷ P v) ={E}=∗
+  (□ ∀ t γ s v, ▷ IP true l γ t s v ={lft_userE}=∗ ▷ P v) ={E}=∗
   (q).[κ] ∗ ∃ γ t v, GPS_aPP IP l κ t s v γ.
 Proof.
   iIntros "#LFT Htok #HINV Hl HP #HP2".
diff --git a/theories/typing/base.v b/theories/typing/base.v
index ab0431c20fb586b3b3b11fa4378fb3bfd40ad2f7..547d7a2b2d9b900d83db6923c748e16203b819c2 100644
--- a/theories/typing/base.v
+++ b/theories/typing/base.v
@@ -1,4 +1,4 @@
-From lrust.lifetime Require Export frac_borrow.
+From stdpp Require Import namespaces.
 From gpfsl.base_logic Require Import na.
 
 (* Last, so that we make sure we shadow the definition of delete for
@@ -7,9 +7,18 @@ From lrust.lang Require Export new_delete.
 
 Open Scope Z_scope.
 
-(* The "user mask" of the lifetime logic, which can be extended for extensions
-   of RustBelt. *)
-Definition lft_userE : coPset := ↑histN.
+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 ∪ ↑histN.
 
 Create HintDb lrust_typing.
 Create HintDb lrust_typing_merge.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 99876a8fb71a2c6fb7e105f7b9e22de6e6f94f9d..efef50ee926c5620d42dccf5a18d3a61770accf7 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -10,7 +10,7 @@ Section fn.
 
   Record fn_params := FP { fp_E : lft → elctx; fp_tys : vec type n; fp_ty : type }.
 
-  Definition FP_wf E (tys : vec type n) `{!TyWfLst tys} ty `{!TyWf ty} :=
+  Definition FP_wf E (tys : vec type n) `{!ListTyWf tys} ty `{!TyWf ty} :=
     FP (λ ϝ, E ϝ ++ tyl_wf_E tys ++ tyl_outlives_E tys ϝ ++
                     ty.(ty_wf_E) ++ ty_outlives_E ty ϝ)
        tys ty.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 65a37602b1b0eca08eb7748f2276273b99cbe778..33810f34b40747832cd2b63cf60adf44b836e282 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -129,12 +129,12 @@ Section arc.
       rewrite monPred_subjectively_unfold. by iExists _. }
     iDestruct (monPred_in_elim with "Inc [Hvs]") as "Hvs";
       first by rewrite -monPred_at_later.
-    rewrite 2!difference_union_distr_l_L difference_diag_L right_id_L
+    rewrite 2!difference_union_distr_l_L difference_diag_L (right_id_L ∅)
             difference_disjoint_L; last solve_ndisj.
-    rewrite difference_disjoint_L; last solve_ndisj.
+    rewrite difference_disjoint_L; last by apply disjoint_union_l; solve_ndisj.
     iMod ("Hν†" with "Hν") as "H". iModIntro. iNext. iApply fupd_trans.
     iMod "H" as "#Hν". iSpecialize ("Hvs" with "Hν").
-    iMod (fupd_mask_mono _ (↑lftN ∪ ↑histN) with "Hvs") as "$"; [set_solver|].
+    iMod (fupd_mask_mono _ (↑lftN ∪ lft_userE) with "Hvs") as "$"; [set_solver|].
     iIntros "{$Hν} !>". iMod ("Hclose" with "[Hν]") as "_"; [|done].
     iLeft. iDestruct (monPred_in_intro with "Hν") as (?) "[? ?]".
     iNext. by iExists _.
@@ -149,7 +149,7 @@ Section arc.
          | _ => False end;
        ty_shr κ tid l :=
          ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗
-           □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ]
+           □ ∀ F q, ⌜↑shrN ∪ ↑lftN ⊆ F⌝ -∗ q.[κ]
              ={F}[F∖↑shrN]▷=∗ q.[κ] ∗ ∃ γi γs γw γsw ν, κ ⊑ ν ∗
                 arc_persist tid ν γi γs γw γsw l' ty ∗
                 ∃ q' ts tw, shared_arc_local l' γs γw ts tw ∗
@@ -288,7 +288,7 @@ Section arc.
          | _ => False end;
        ty_shr κ tid l :=
          ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗
-           □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ]
+           □ ∀ F q, ⌜↑shrN ∪ ↑lftN ⊆ F⌝ -∗ q.[κ]
              ={F}[F∖↑shrN]▷=∗ q.[κ] ∗ ∃ γi γs γw γsw ν,
                 arc_persist tid ν γi γs γw γsw l' ty ∗
                 ∃ q' ts tw, shared_arc_local l' γs γw ts tw ∗
@@ -872,7 +872,9 @@ Section arc.
       iDestruct "Hpersist" as "(? & ? & H†)". wp_bind (_ <- _)%E.
       iDestruct "Hdrop" as "[Hν Hdrop]". iSpecialize ("H†" with "Hν").
       iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [done..|set_solver|].
-      iDestruct "Hown" as (???) "(_ & Hlen & _)". wp_write. iIntros "(#Hν & Hown & H†)!>".
+      iDestruct "Hown" as (???) "(_ & Hlen & _)".
+      iApply (wp_mask_mono _ (↑histN)); [set_solver+|].
+      wp_write. iIntros "(#Hν & Hown & H†)!>".
       wp_seq. wp_op. wp_op. iDestruct "Hown" as (?) "[H↦ Hown]".
       iDestruct (ty_size_eq with "Hown") as %?. rewrite Max.max_0_r.
       iDestruct "Hlen" as %[= ?]. wp_apply (wp_memcpy with "[$H↦1 $H↦]"); [auto..|].
@@ -976,7 +978,8 @@ Section arc.
       rewrite heap_mapsto_vec_cons. iDestruct "Hr" as "[Hr0 Hr1]".
       iDestruct "Hpersist" as "(Ha & _ & H†)". wp_bind (_ <- _)%E.
       iSpecialize ("H†" with "Hν").
-      iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [done..|set_solver|].
+      iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [done..|set_solver+|].
+      iApply (wp_mask_mono _ (↑histN)); [set_solver+|].
       wp_write. iIntros "(#Hν & Hown & H†) !>". wp_seq. wp_op. wp_op.
       rewrite -(firstn_skipn ty.(ty_size) vl0) heap_mapsto_vec_app.
       iDestruct "Hr1" as "[Hr1 Hr2]". iDestruct "Hown" as (vl) "[Hrc' Hown]".
@@ -1158,8 +1161,8 @@ Section arc.
       iApply type_jump; solve_typing.
     - iIntros "[Hν Hweak]". wp_case. iSpecialize ("Hc" with "Hν"). wp_bind (new _).
       iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); [done..|set_solver|].
-      wp_apply wp_new=>//. lia. iIntros (l) "(H† & Hlvl) (#Hν & Hown & H†') !>".
-      rewrite -!lock Nat2Z.id.
+      wp_apply wp_new=>//; [set_solver+|lia|].
+      iIntros (l) "(H† & Hlvl) (#Hν & Hown & H†') !>". rewrite -!lock Nat2Z.id.
       wp_let. wp_op. rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
       iDestruct "Hlvl" as "(Hrc0 & Hrc1 & Hrc2)". wp_write. wp_op. wp_write.
       wp_op. wp_op. iDestruct "Hown" as (vl) "[H↦ Hown]".
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index d26dc8f0f2d95c9447cbd75c6c97715bd3114a05..6452d0de2bf18d8da4472da7bd8ff09b07b8383f 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -54,8 +54,8 @@ Section mutex.
       iExists vl. iFrame. }
     clear b vl. iMod (bor_sep with "LFT Hbor") as "[Hl Hbor]"; first done.
     iMod (lock_proto_create mutexN l q κ (&{κ}((l +ₗ 1) ↦∗: ty.(ty_own) tid))%I
-            with "LFT Htok hInv Hl [Hbor]")
-       as "[$ Hproto]"; [solve_ndisj|done..|].
+            with "LFT Htok hInv Hl Hbor")
+      as "[$ Hproto]"; [solve_ndisj|done|set_solver|].
     iExists κ. iFrame "Hproto ". by iApply lft_incl_refl.
   Qed.
   Next Obligation.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 6e31e1e922c5082e0c575779f3f9967a9bb8ae1d..471c21e6eaa45ef07dfb3b01ec9d7dd89d197f72 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -37,7 +37,7 @@ Section mguard.
          | _ => False end;
        ty_shr κ tid l :=
          ∃ (l':loc), &frac{κ}(λ q', l ↦{q'} #l') ∗
-            □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α⊓κ]
+            □ ∀ F q, ⌜↑shrN ∪ ↑lftN ⊆ F⌝ -∗ q.[α⊓κ]
                 ={F}[F∖↑shrN]▷=∗ ty.(ty_shr) (α⊓κ) tid (l' +ₗ 1) ∗ q.[α⊓κ]
     |}%I.
   Next Obligation. by iIntros (? ty tid [|[[]|][]]) "H". Qed.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index e10a8fc092b3deda5cdee2f2660c01db5fd260a4..9a965176702476d51da9a44b44673aa1f7ca16e2 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -122,7 +122,7 @@ Section rc.
          | _ => False end;
        ty_shr κ tid l :=
          ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗
-           □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ]
+           □ ∀ F q, ⌜↑shrN ∪ ↑lftN ⊆ F⌝ -∗ q.[κ]
              ={F}[F∖↑shrN]▷=∗ q.[κ] ∗ ∃ γ ν q', κ ⊑ ν ∗
                 rc_persist tid ν γ l' ty ∗
                 &na{κ, tid, rc_shrN}(⎡own γ (rc_tok q')⎤)
@@ -306,7 +306,7 @@ Section code.
                last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
              iModIntro. iNext. iMod "H†".
              iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
-             { set_solver-. }
+             { set_solver+. }
              iMod "Hclose2" as "_". iModIntro.
              iMod ("Hclose" with "[Hst $Hna]") as "$"; first by iExists _; iFrame.
              iModIntro. iNext. iDestruct "Hty" as (vl) "[??]". iExists _. iFrame.
@@ -321,7 +321,7 @@ Section code.
                   last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
                 iModIntro. iNext. iMod "H†".
                 iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
-                { set_solver-. }
+                { set_solver+. }
                 iMod "Hclose2" as "_". iModIntro.
                 iMod (own_update_2 with "Hst Htok") as "Hst".
                 { apply auth_update_dealloc, prod_local_update_1,
@@ -342,7 +342,7 @@ Section code.
             last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
           iModIntro. iNext. iMod "H†".
           iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
-          { set_solver-. }
+          { set_solver+. }
           iMod "Hclose2" as "_". iModIntro.
           iMod ("Hclose" with "[Hst $Hna Hl1 Hl2]") as "$";
             first by iExists _; iFrame; iFrame.
@@ -1047,7 +1047,7 @@ Section code.
         iApply type_jump; solve_typing.
       + wp_op; case_bool_decide; first lia. wp_if. wp_op. rewrite shift_loc_0. wp_write. wp_op.
         wp_op. wp_write. wp_bind (new _). iSpecialize ("Hrc" with "Hl1 Hl2").
-        iApply (wp_step_fupd with "Hrc"); [done..|]. iApply wp_new; [done|lia|done|].
+        iApply (wp_step_fupd with "Hrc"); [done..|]. iApply wp_new; [set_solver+|lia|done|].
         rewrite -!lock Nat2Z.id.
         iNext. iIntros (lr) "/= ([H†|%] & H↦lr) [Hty Hproto] !>"; last lia.
         rewrite 2!heap_mapsto_vec_cons. iDestruct "H↦lr" as "(Hlr1 & Hlr2 & Hlr3)".
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 4dc0ad6348306762d2e718cc1cd104b66e1ccc19..5f358ab2a7c9550e9af722b1e8b3ee6b3f0bc30c 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -18,7 +18,7 @@ Section weak.
          | _ => False end;
        ty_shr κ tid l :=
          ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗
-           □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ]
+           □ ∀ F q, ⌜↑shrN ∪ ↑lftN ⊆ F⌝ -∗ q.[κ]
              ={F}[F∖↑shrN]▷=∗ q.[κ] ∗ ∃ γ ν, rc_persist tid ν γ l' ty ∗
                 &na{κ, tid, rc_shrN}(⎡own γ weak_tok⎤)
     |}%I.
@@ -470,7 +470,7 @@ Section code.
     iMod (lft_create with "LFT") as (ν) "[Hν #Hν†]"; first done.
     iPoseProof ("Hν†" with "Hν") as "H†". wp_bind (_ <- _)%E.
     iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [set_solver-..|].
-    wp_write. iIntros "#Hν !>". wp_seq.
+    iApply (wp_mask_mono _ (↑histN)); [set_solver+|]. wp_write. iIntros "#Hν !>". wp_seq.
     iApply (type_type _ _ _ [ #lw ◁ box (weak ty)]
         with "[] LFT HE Hna HL Hk [> -]"); last first.
     { rewrite tctx_interp_singleton tctx_hasty_val' //=. iFrame.
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 5136a8e21a28c72dcf395fc9a57c75e4bba67df3..65cd958d91e938193286e78cf7f5c3bf3d1d990c 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -32,7 +32,7 @@ Section refmut.
        ty_shr κ tid l :=
          ∃ (lv lrc : loc),
            &frac{κ} (λ q, l↦∗{q} [ #lv; #lrc]) ∗
-           □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α ⊓ κ]
+           □ ∀ F q, ⌜↑shrN ∪ ↑lftN ⊆ F⌝ -∗ q.[α ⊓ κ]
              ={F}[F∖↑shrN]▷=∗ ty.(ty_shr) (α ⊓ κ) tid lv ∗ q.[α ⊓ κ] |}%I.
   Next Obligation.
     iIntros (???[|[[]|][|[[]|][]]]); try iIntros "[]". by iIntros "_".
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 298264f6ee26c34ab4d126a331da1df75af39574..a8fb584f541a267c39a003c1c81eb6a8e52b7ad2 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -166,7 +166,7 @@ Section rwlock_inv.
     (γs: gname) (α : lft) (tyO: vProp) (tyS: lft → vProp)
     : interpO Σ unitProtocol :=
     (λ pb l γ t _ vs, ∃ st, ⌜vs = #(Z_of_rwlock_st st)⌝ ∗
-       (□ (∀ κ q E, ⌜lftE ⊆ E⌝ -∗ &{κ}tyO -∗ q.[κ] ={E}=∗ (□ tyS κ) ∗ q.[κ])) ∗
+       (□ (∀ κ q E, ⌜↑lftN ⊆ E⌝ -∗ &{κ}tyO -∗ q.[κ] ={E}=∗ (□ tyS κ) ∗ q.[κ])) ∗
        if pb
        then rwown γs (st_global st) ∗
             match st return _ with
@@ -177,7 +177,7 @@ Section rwlock_inv.
             | Some (inr (ν, q, n)) => (* Locked for read. *)
                   GPS_SWSharedWriter l t () #(Z.pos n) γ ∗
                   ∃ q', □ (1.[ν] ={↑lftN ∪ lft_userE}[lft_userE]▷=∗ [†ν]) ∗
-                    ([†ν] ={↑lftN ∪ ↑histN}=∗ &{α}tyO) ∗
+                    ([†ν] ={↑lftN ∪ lft_userE}=∗ &{α}tyO) ∗
                     (□ tyS (α ⊓ ν)) ∗ ⌜(q + q')%Qp = 1%Qp⌝ ∗
                     q'.[ν] ∗
                     GPS_SWSharedReader l t () #(Z.pos n) q' γ
@@ -253,7 +253,7 @@ Section rwlock_inv.
       + iApply "EqS". by iApply "Hshr".
   Qed.
 
-  Lemma rwlock_proto_create l q tid α ty E (SUB: lftE ⊆ E):
+  Lemma rwlock_proto_create l q tid α ty E (SUB: ↑lftN ⊆ E):
     ⎡ lft_ctx ⎤ -∗
     (q).[α] -∗ ▷ ⎡ hist_inv ⎤ -∗
     &{α} ((l +ₗ 1) ↦∗{1}: ty_own ty tid)%I -∗
@@ -267,7 +267,7 @@ Section rwlock_inv.
     { iIntros "!>". by iApply (bi.iff_refl True%I). }
     iAssert (□ (∀ α', tyS α' ↔ ty.(ty_shr) α' tid (l +ₗ 1)))%I as "#EqS".
     { iIntros "!>" (?). by iApply (bi.iff_refl True%I). }
-    iAssert (□ (∀ κ q' E', ⌜lftE ⊆ E'⌝ -∗ &{κ} tyO -∗
+    iAssert (□ (∀ κ q' E', ⌜↑lftN ⊆ E'⌝ -∗ &{κ} tyO -∗
                            (q').[κ] ={E'}=∗ (□ tyS κ) ∗ (q').[κ]))%I as "#Share".
     { iIntros "!>" (????) "tyO tok".
       by iMod (ty_share with "LFT tyO tok") as "[#? $]". }
@@ -279,8 +279,8 @@ Section rwlock_inv.
                 | None => (* Not locked. *)
                       &{α}tyO
                 | Some (inr (ν, q, n)) => (* Locked for read. *)
-                      ∃ q', □ (1.[ν] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ [†ν]) ∗
-                        ([†ν] ={↑lftN ∪ ↑histN}=∗ &{α}tyO) ∗
+                      ∃ q', □ (1.[ν] ={↑lftN ∪ lft_userE}[lft_userE]▷=∗ [†ν]) ∗
+                        ([†ν] ={↑lftN ∪ lft_userE}=∗ &{α}tyO) ∗
                         (□ tyS (α ⊓ ν)) ∗ ⌜(q + q')%Qp = 1%Qp⌝ ∗
                         q'.[ν]
                 | _ => (* Locked for write. *) True
@@ -325,7 +325,7 @@ Section rwlock_inv.
     iMod (GPS_aSP_Init rwlockN (rwlock_interp γs α tyO tyS) rwlock_noCAS
               l α () _ (P γs) (λ _ _ _, True)%I
               with "LFT Htok HINV H [] []") as "[$ Hproto]";
-          [solve_ndisj|done|..].
+          [solve_ndisj|done|set_solver|..].
     { iIntros (t γ v) "P W". iSplitR ""; [|done].
       iDestruct "P" as (st) "[>% [Hst H]]". subst v. iExists _.
       iFrame "Share Hst". iSplitL ""; [done|].
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 9202034f9b38b83c01e4d3333d10913e9933da50..6134729ff4e4b4b7805e01ad5ff4a956747319c4 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -267,7 +267,7 @@ Section rwlock_functions.
           iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #H†]". solve_ndisj.
           iMod (rwown_update_write_read ν γs with "g") as "[g rst]".
           iDestruct (lft_intersect_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
-          iApply (fupd_mask_mono (↑lftN ∪ ↑histN)).
+          iApply (fupd_mask_mono (↑lftN ∪ lft_userE)).
           { apply union_subseteq; split; solve_ndisj. }
           iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hown") as "[Hst Hh]";
             [apply union_subseteq_l|iApply lft_intersect_incl_l|].
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 26ce0133be4798412848c020ae6623b971f10d1c..b76a91d4482e148e523a3c275d8b66d2d67cb619 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -125,7 +125,7 @@ Section rwlockreadguard_functions.
         { rewrite /Q1 Eqst. by iIntros "!> $". }
         destruct CASE as [[??]|[[q0 ?] Eqn]]; [subst q' n|subst q'].
         - rewrite Hqrq'. iMod (rwown_update_read_dealloc_1 with "H● H◯") as "H●".
-          iApply (step_fupd_mask_mono (↑lftN ∪ ↑histN) _ (↑histN));
+          iApply (step_fupd_mask_mono (↑lftN ∪ lft_userE) _ lft_userE);
             [solve_ndisj|apply union_least; solve_ndisj|..].
           iMod ("H†" with "Hν") as "Hν". iIntros "!> !>". iMod "Hν".
           iMod ("Hh" with "Hν") as "Hb". iModIntro.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index dac7663d6e8bf8f720fd97ef9c9f2267a93b475f..77b1f4385242342f7bea37f712bbda7a91e1ca96 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -31,7 +31,7 @@ Section rwlockwriteguard.
        ty_shr κ tid l :=
          ∃ (l' : loc),
            &frac{κ} (λ q, l↦∗{q} [ #l']) ∗
-           □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α ⊓ κ] ={F}[F∖↑shrN]▷=∗
+           □ ∀ F q, ⌜↑shrN ∪ ↑lftN ⊆ F⌝ -∗ q.[α ⊓ κ] ={F}[F∖↑shrN]▷=∗
                ty.(ty_shr) (α ⊓ κ) tid (l' +ₗ 1) ∗ q.[α ⊓ κ] |}%I.
   Next Obligation. by iIntros (???[|[[]|][]]) "?". Qed.
   Next Obligation.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index edc3e8536ca6091e1d86f60238145078498432d9..1fa5fb5ccb50910acd5dd87a9af68998eea7c425 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -61,7 +61,7 @@ Section own.
          end%I;
        ty_shr κ tid l :=
          (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
-            □ (∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ] ={F}[F∖↑shrN]▷=∗
+            □ (∀ F q, ⌜↑shrN ∪ ↑lftN ⊆ F⌝ -∗ q.[κ] ={F}[F∖↑shrN]▷=∗
                             ty.(ty_shr) κ tid l' ∗ q.[κ]))%I |}.
   Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed.
   Next Obligation.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index cde5ec3ba8adee1a01525cab3e699910e19ddbe6..0b1bc8e40bc6608ff6330549e11de2f4e1c06aa6 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -155,7 +155,7 @@ Section product.
   Definition product := foldr product2 unit0.
   Definition unit := product [].
 
-  Global Instance product_wf tyl `{!TyWfLst tyl} : TyWf (product tyl) :=
+  Global Instance product_wf tyl `{!ListTyWf tyl} : TyWf (product tyl) :=
     { ty_lfts := tyl_lfts tyl; ty_wf_E := tyl_wf_E tyl }.
 
   Lemma outlives_product ty1 ty2 ϝ `{!TyWf ty1, !TyWf ty2} :
@@ -178,11 +178,11 @@ Section product.
   Lemma product_proper' E L tyl1 tyl2 :
     Forall2 (eqtype E L) tyl1 tyl2 → eqtype E L (product tyl1) (product tyl2).
   Proof. apply product_proper. Qed.
-  Global Instance product_copy tys : LstCopy tys → Copy (product tys).
+  Global Instance product_copy tys : ListCopy tys → Copy (product tys).
   Proof. induction 1; apply _. Qed.
-  Global Instance product_send tys : LstSend tys → Send (product tys).
+  Global Instance product_send tys : ListSend tys → Send (product tys).
   Proof. induction 1; apply _. Qed.
-  Global Instance product_sync tys : LstSync tys → Sync (product tys).
+  Global Instance product_sync tys : ListSync tys → Sync (product tys).
   Proof. induction 1; apply _. Qed.
 
   Definition product_cons ty tyl :
@@ -251,7 +251,7 @@ Section typing.
     eqtype E L (Π[Π tyl1; Π tyl2]) (Π(tyl1 ++ tyl2)).
   Proof. by rewrite -prod_flatten_r -prod_flatten_l. Qed.
 
-  Lemma ty_outlives_E_elctx_sat_product E L tyl {Wf : TyWfLst tyl} α:
+  Lemma ty_outlives_E_elctx_sat_product E L tyl {Wf : ListTyWf tyl} α:
     elctx_sat E L (tyl_outlives_E tyl α) →
     elctx_sat E L (ty_outlives_E (Π tyl) α).
   Proof.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index eb5075dfbd6643d31c237fd2f853d4a25ab12f50..3027a1a8fac6d1176e098dd7a658cc3b7a3edac3 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -1,7 +1,8 @@
 From iris.algebra Require Import numbers.
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
-From lrust.typing Require Import type_context lft_contexts product own uniq_bor shr_bor.
+From lrust.typing Require Import type_context lft_contexts product own uniq_bor.
+From lrust.typing Require Import shr_bor.
 Set Default Proof Using "Type".
 
 Section product_split.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index faada6582cd2024af0d752b0d0f9eb0f59f227d5..4e81d04ad33518c35f918acac50a420c07b4f8aa 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -68,7 +68,7 @@ Section typing.
 
   (** Writing and Reading **)
   Definition typed_write_def (E : elctx) (L : llctx) (ty1 ty ty2 : type) : vPropI Σ :=
-    (□ ∀ v tid F qmax qL, ⌜lftE ∪ (↑lrustN) ⊆ F⌝ →
+    (□ ∀ v tid F qmax qL, ⌜↑lftN ∪ (↑lrustN) ⊆ F⌝ →
       ⎡lft_ctx⎤ -∗ elctx_interp E -∗ llctx_interp_noend qmax L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
         ∃ (l : loc) vl, ⌜length vl = ty.(ty_size) ∧ v = #l⌝ ∗ l ↦∗ vl ∗
           (▷ l ↦∗: ty.(ty_own) tid ={F}=∗
@@ -88,7 +88,7 @@ Section typing.
      that nobody could possibly have changed the vl (because only half the
      fraction was given). So we go with the definition that is easier to prove. *)
   Definition typed_read_def (E : elctx) (L : llctx) (ty1 ty ty2 : type) : vPropI Σ :=
-    (□ ∀ v tid F qmax qL, ⌜lftE ∪ ↑lrustN ⊆ F⌝ →
+    (□ ∀ v tid F qmax qL, ⌜↑lftN ∪ ↑lrustN ⊆ F⌝ →
       ⎡lft_ctx⎤ -∗ elctx_interp E -∗ na_own tid F -∗
       llctx_interp_noend qmax L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
         ∃ (l : loc) vl q, ⌜v = #l⌝ ∗ l ↦∗{q} vl ∗ ▷ ty.(ty_own) tid vl ∗
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 64a46e93d93aac23d7309b4cf2686f908e6fce40..ce46d4fc1e1751acc6d38096613dbf8b7594346f 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -9,10 +9,10 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Class typePreG Σ := PreTypeG {
-  type_heapG :> noprolPreG Σ;
-  type_lftG :> lftPreG Σ view_Lat;
+  type_preG_heapG :> noprolPreG Σ;
+  type_preG_lftG :> lftPreG Σ view_Lat;
   type_preG_na_invG :> na_invG view_Lat Σ;
-  type_frac_borrowG :> frac_borG Σ
+  type_preG_frac_borG :> frac_borG Σ
 }.
 
 Definition typeΣ : gFunctors :=
@@ -40,7 +40,8 @@ Section type_soundness.
       - destruct toval as [v ?%nopro_lang.to_base_val]. eauto.
       - eauto. }
     apply: (noprol_adequacy' _ _ (λ x, True))=>? tid1.
-    iMod (lft_init _ lft_userE) as (?) "#LFT"; [done|solve_ndisj|].
+    iMod (lft_init _ lft_userE) as (?) "#LFT";
+      [done|apply disjoint_union_r; solve_ndisj|].
     iMod na_alloc as (tid2) "Htl". set (Htype := TypeG _ _ _ _ _).
     set (tid := {| tid_na_inv_pool := tid2; tid_tid := tid1 |}).
     wp_bind (of_val main). iApply (wp_wand with "[Htl]").
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 4d42bb78362aae88eca95cb46c64f082a69da907..df33cd6d8a7c550c5513899713cdcdc8a30104d9 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -84,7 +84,7 @@ Section sum.
     - iApply ((nth i tyl emp0).(ty_shr_mono) with "Hord"); done.
   Qed.
 
-  Global Instance sum_wf tyl `{!TyWfLst tyl} : TyWf (sum tyl) :=
+  Global Instance sum_wf tyl `{!ListTyWf tyl} : TyWf (sum tyl) :=
     { ty_lfts := tyl_lfts tyl; ty_wf_E := tyl_wf_E tyl }.
 
   Global Instance sum_type_ne n : Proper (Forall2 (type_dist2 n) ==> type_dist2 n) sum.
@@ -174,7 +174,7 @@ Section sum.
     nth i [] d = d.
   Proof. by destruct i. Qed.
 
-  Global Instance sum_copy tyl : LstCopy tyl → Copy (sum tyl).
+  Global Instance sum_copy tyl : ListCopy tyl → Copy (sum tyl).
   Proof.
     intros HFA. split.
     - intros tid vl.
@@ -215,7 +215,7 @@ Section sum.
         iMod ("Hclose" with "[$Hown1 $Hown2]") as "$". by iFrame.
   Qed.
 
-  Global Instance sum_send tyl : LstSend tyl → Send (sum tyl).
+  Global Instance sum_send tyl : ListSend tyl → Send (sum tyl).
   Proof.
     iIntros (Hsend tid1 tid2 vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
     iExists _, _, _. iSplit; first done. iSplit; first done. iApply @send_change_tid; last done.
@@ -223,7 +223,7 @@ Section sum.
     iIntros (???) "[]".
   Qed.
 
-  Global Instance sum_sync tyl : LstSync tyl → Sync (sum tyl).
+  Global Instance sum_sync tyl : ListSync tyl → Sync (sum tyl).
   Proof.
     iIntros (Hsync κ tid1 tid2 l) "H". iDestruct "H" as (i) "[Hframe Hown]".
     iExists _. iFrame "Hframe". iApply @sync_change_tid; last done.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 8528f6d536a3940e089e75ca5f0f9b15fa46a14d..183eb2d280b55a50bd721909ff34b2b57b59a60f 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -14,7 +14,6 @@ Class typeG Σ := TypeG {
   type_frac_borrowG :> frac_borG Σ
 }.
 
-Definition lftE : coPset := ↑lftN.
 Definition lrustN := nroot .@ "lrust".
 Definition shrN  := lrustN .@ "shr".
 
@@ -45,7 +44,7 @@ Record type `{!typeG Σ} :=
        nicer (they would otherwise require a "∨ □|=>[†κ]"), and (b) so that
        we can have emp == sum [].
      *)
-    ty_share E κ l tid q : lftE ⊆ E →
+    ty_share E κ l tid q : ↑lftN ⊆ E →
       ⎡lft_ctx⎤ -∗ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗
       ty_shr κ tid l ∗ q.[κ];
     ty_shr_mono κ κ' tid l :
@@ -79,34 +78,34 @@ Proof.
 Qed.
 
 (* Lift TyWf to lists.  We cannot use `Forall` because that one is restricted to Prop. *)
-Inductive TyWfLst `{!typeG Σ} : list type → Type :=
-| tyl_wf_nil : TyWfLst []
-| tyl_wf_cons ty tyl `{!TyWf ty, !TyWfLst tyl} : TyWfLst (ty::tyl).
-Existing Class TyWfLst.
-Existing Instances tyl_wf_nil tyl_wf_cons.
+Inductive ListTyWf `{!typeG Σ} : list type → Type :=
+| list_ty_wf_nil : ListTyWf []
+| list_ty_wf_cons ty tyl `{!TyWf ty, !ListTyWf tyl} : ListTyWf (ty::tyl).
+Existing Class ListTyWf.
+Existing Instances list_ty_wf_nil list_ty_wf_cons.
 
-Fixpoint tyl_lfts `{!typeG Σ} tyl {WF : TyWfLst tyl} : list lft :=
+Fixpoint tyl_lfts `{!typeG Σ} tyl {WF : ListTyWf tyl} : list lft :=
   match WF with
-  | tyl_wf_nil => []
-  | tyl_wf_cons ty [] => ty.(ty_lfts)
-  | tyl_wf_cons ty tyl => ty.(ty_lfts) ++ tyl.(tyl_lfts)
+  | list_ty_wf_nil => []
+  | list_ty_wf_cons ty [] => ty.(ty_lfts)
+  | list_ty_wf_cons ty tyl => ty.(ty_lfts) ++ tyl.(tyl_lfts)
   end.
 
-Fixpoint tyl_wf_E `{!typeG Σ} tyl {WF : TyWfLst tyl} : elctx :=
+Fixpoint tyl_wf_E `{!typeG Σ} tyl {WF : ListTyWf tyl} : elctx :=
   match WF with
-  | tyl_wf_nil => []
-  | tyl_wf_cons ty [] => ty.(ty_wf_E)
-  | tyl_wf_cons ty tyl => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
+  | list_ty_wf_nil => []
+  | list_ty_wf_cons ty [] => ty.(ty_wf_E)
+  | list_ty_wf_cons ty tyl => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
   end.
 
-Fixpoint tyl_outlives_E `{!typeG Σ} tyl {WF : TyWfLst tyl} (κ : lft) : elctx :=
+Fixpoint tyl_outlives_E `{!typeG Σ} tyl {WF : ListTyWf tyl} (κ : lft) : elctx :=
   match WF with
-  | tyl_wf_nil => []
-  | tyl_wf_cons ty [] => ty_outlives_E ty κ
-  | tyl_wf_cons ty tyl => ty_outlives_E ty κ ++ tyl.(tyl_outlives_E) κ
+  | list_ty_wf_nil => []
+  | list_ty_wf_cons ty [] => ty_outlives_E ty κ
+  | list_ty_wf_cons ty tyl => ty_outlives_E ty κ ++ tyl.(tyl_outlives_E) κ
   end.
 
-Lemma tyl_outlives_E_elctx_sat `{!typeG Σ} E L tyl {WF : TyWfLst tyl} α β :
+Lemma tyl_outlives_E_elctx_sat `{!typeG Σ} E L tyl {WF : ListTyWf tyl} α β :
   tyl_outlives_E tyl β ⊆+ E →
   lctx_lft_incl E L α β →
   elctx_sat E L (tyl_outlives_E tyl α).
@@ -178,7 +177,7 @@ Section ofe.
   Let P (x : T) : Prop :=
     (∀ κ tid l, Persistent (x.2 κ tid l)) ∧
     (∀ tid vl, x.1.2 tid vl -∗ ⌜length vl = x.1.1⌝) ∧
-    (∀ E κ l tid q, lftE ⊆ E →
+    (∀ E κ l tid q, ↑lftN ⊆ E →
       ⎡lft_ctx⎤ -∗ &{κ} (l ↦∗: λ vs, x.1.2 tid vs) -∗
       q.[κ] ={E}=∗ x.2 κ tid l ∗ q.[κ]) ∧
     (∀ κ κ' tid l, κ' ⊑ κ -∗ x.2 κ tid l -∗ x.2 κ' tid l).
@@ -398,7 +397,7 @@ Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
 Class Copy `{!typeG Σ} (t : type) := {
   copy_persistent tid vl : Persistent (t.(ty_own) tid vl);
   copy_shr_acc κ tid E F l q :
-    lftE ∪ ↑shrN ⊆ E → shr_locsE l (t.(ty_size) + 1) ⊆ F →
+    ↑lftN ∪ ↑shrN ⊆ E → shr_locsE l (t.(ty_size) + 1) ⊆ F →
     ⎡lft_ctx⎤ -∗ t.(ty_shr) κ tid l -∗ na_own tid F -∗ q.[κ] ={E}=∗
        ∃ q', na_own tid (F ∖ shr_locsE l t.(ty_size)) ∗
          ▷(l ↦∗{q'}: t.(ty_own) tid) ∗
@@ -408,31 +407,31 @@ Class Copy `{!typeG Σ} (t : type) := {
 Existing Instances copy_persistent.
 Instance: Params (@Copy) 2 := {}.
 
-Class LstCopy `{!typeG Σ} (tys : list type) := lst_copy : Forall Copy tys.
-Instance: Params (@LstCopy) 2 := {}.
-Global Instance lst_copy_nil `{!typeG Σ} : LstCopy [] := List.Forall_nil _.
+Class ListCopy `{!typeG Σ} (tys : list type) := lst_copy : Forall Copy tys.
+Instance: Params (@ListCopy) 2 := {}.
+Global Instance lst_copy_nil `{!typeG Σ} : ListCopy [] := List.Forall_nil _.
 Global Instance lst_copy_cons `{!typeG Σ} ty tys :
-  Copy ty → LstCopy tys → LstCopy (ty :: tys) := List.Forall_cons _ _ _.
+  Copy ty → ListCopy tys → ListCopy (ty :: tys) := List.Forall_cons _ _ _.
 
 Class Send `{!typeG Σ} (t : type) :=
   send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl -∗ t.(ty_own) tid2 vl.
 Instance: Params (@Send) 2 := {}.
 
-Class LstSend `{!typeG Σ} (tys : list type) := lst_send : Forall Send tys.
-Instance: Params (@LstSend) 2 := {}.
-Global Instance lst_send_nil `{!typeG Σ} : LstSend [] := List.Forall_nil _.
+Class ListSend `{!typeG Σ} (tys : list type) := lst_send : Forall Send tys.
+Instance: Params (@ListSend) 2 := {}.
+Global Instance lst_send_nil `{!typeG Σ} : ListSend [] := List.Forall_nil _.
 Global Instance lst_send_cons `{!typeG Σ} ty tys :
-  Send ty → LstSend tys → LstSend (ty :: tys) := List.Forall_cons _ _ _.
+  Send ty → ListSend tys → ListSend (ty :: tys) := List.Forall_cons _ _ _.
 
 Class Sync `{!typeG Σ} (t : type) :=
   sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l -∗ t.(ty_shr) κ tid2 l.
 Instance: Params (@Sync) 2 := {}.
 
-Class LstSync `{!typeG Σ} (tys : list type) := lst_sync : Forall Sync tys.
-Instance: Params (@LstSync) 2 := {}.
-Global Instance lst_sync_nil `{!typeG Σ} : LstSync [] := List.Forall_nil _.
+Class ListSync `{!typeG Σ} (tys : list type) := lst_sync : Forall Sync tys.
+Instance: Params (@ListSync) 2 := {}.
+Global Instance lst_sync_nil `{!typeG Σ} : ListSync [] := List.Forall_nil _.
 Global Instance lst_sync_cons `{!typeG Σ} ty tys :
-  Sync ty → LstSync tys → LstSync (ty :: tys) := List.Forall_cons _ _ _.
+  Sync ty → ListSync tys → ListSync (ty :: tys) := List.Forall_cons _ _ _.
 
 Section type.
   Context `{!typeG Σ}.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index f52ac69f24a049ba2a9406081144294cfe8571f8..1bd53a5299aeb1f0ebb5122d59c799ab53491652 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -286,7 +286,7 @@ Section case.
     by iApply type_seq; [eapply type_sum_memcpy_instr, Hr|done|done].
   Qed.
 
-  Lemma ty_outlives_E_elctx_sat_sum E L tyl {Wf : TyWfLst tyl} α:
+  Lemma ty_outlives_E_elctx_sat_sum E L tyl {Wf : ListTyWf tyl} α:
     elctx_sat E L (tyl_outlives_E tyl α) →
     elctx_sat E L (ty_outlives_E (sum tyl) α).
   Proof.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index db21e0b94d7b04568eeddfc00d14676451258bea..4747f0f7816466a0f78190296dbecd1936663f7e 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -15,7 +15,7 @@ Section uniq_bor.
          end;
        ty_shr κ' tid l :=
          ∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
-           □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ⊓κ']
+           □ ∀ F q, ⌜↑shrN ∪ ↑lftN ⊆ F⌝ -∗ q.[κ⊓κ']
                ={F}[F∖↑shrN]▷=∗ ty.(ty_shr) (κ⊓κ') tid l' ∗ q.[κ⊓κ']
     |}%I.
   Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed.
diff --git a/theories/typing/util.v b/theories/typing/util.v
index 424110d1b84983cc3ec297eb0c0c4a5825aeb113..793773224b5e9c9d3d4c6c174f25c1aca9aa7838 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -24,10 +24,10 @@ Section util.
    *)
 
   Lemma delay_sharing_later N κ l ty tid :
-    lftE ⊆ N →
+    ↑lftN ⊆ N →
     ⎡lft_ctx⎤ -∗ &{κ}(▷ l ↦∗: ty_own ty tid) ={N}=∗
        □ ∀ (F : coPset) (q : Qp),
-       ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ] ={F}[F ∖ ↑shrN]▷=∗ ty.(ty_shr) κ tid l ∗ (q).[κ].
+       ⌜↑shrN ∪ ↑lftN ⊆ F⌝ -∗ (q).[κ] ={F}[F ∖ ↑shrN]▷=∗ ty.(ty_shr) κ tid l ∗ (q).[κ].
   Proof.
     iIntros (?) "#LFT Hbor". rewrite bor_unfold_idx.
     iDestruct (monPred_in_intro with "Hbor") as (V) "[#Hin Hbor]".
@@ -54,10 +54,10 @@ Section util.
   Qed.
 
   Lemma delay_sharing_nested N κ κ' κ'' l ty tid :
-    lftE ⊆ N →
+    ↑lftN ⊆ N →
     ⎡lft_ctx⎤ -∗ ▷ (κ'' ⊑ κ ⊓ κ') -∗ &{κ'}(&{κ}(l ↦∗: ty_own ty tid)) ={N}=∗
        □ ∀ (F : coPset) (q : Qp),
-       ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ''] ={F}[F ∖ ↑shrN]▷=∗ ty.(ty_shr) κ'' tid l ∗ (q).[κ''].
+       ⌜↑shrN ∪ ↑lftN ⊆ F⌝ -∗ (q).[κ''] ={F}[F ∖ ↑shrN]▷=∗ ty.(ty_shr) κ'' tid l ∗ (q).[κ''].
   Proof.
     iIntros (?) "#LFT Hincl Hbor". rewrite bor_unfold_idx.
     iCombine "Hincl Hbor" as "Hinclbor".