diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 880b4c42c32e65d9c322cce375e3139066b99e3b..0564a8e7c8c40e622712bc28cc2f87487f10c2e4 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -19,7 +19,7 @@ Module Export lifetime : lifetime_sig.
   Include in_at_borrow.
 End lifetime.
 
-Notation lft_intersect_list l := (foldr lft_intersect static l).
+Notation lft_intersect_list l := (foldr (⊓) static l).
 
 Instance lft_inhabited : Inhabited lft := populate static.
 
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 22432542fd84f1d92c9781d10cbb5e949d11e026..8899796cda252c040875843edd6461b573917c4f 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -24,7 +24,7 @@ Module Type lifetime_sig.
   (** Definitions *)
   Parameter lft : Type.
   Parameter static : lft.
-  Global Declare Instance lft_intersect : Meet lft.
+  Declare Instance lft_intersect : Meet lft.
 
   Section defs.
   Context {Σ : gFunctors} {Lat}.
@@ -64,12 +64,12 @@ Module Type lifetime_sig.
   Global Declare Instance lft_inhabited : Inhabited lft.
   Global Declare Instance bor_idx_inhabited : Inhabited bor_idx.
 
-  Global Declare Instance lft_intersect_comm : Comm eq lft_intersect.
-  Global Declare Instance lft_intersect_assoc : Assoc eq lft_intersect.
-  Global Declare Instance lft_intersect_inj_1 κ : Inj eq eq (lft_intersect κ).
-  Global Declare Instance lft_intersect_inj_2 κ : Inj eq eq (λ κ', lft_intersect κ' κ).
-  Global Declare Instance lft_intersect_left_id : LeftId eq static lft_intersect.
-  Global Declare Instance lft_intersect_right_id : RightId eq static lft_intersect.
+  Global Declare Instance lft_intersect_comm : Comm (A:=lft) eq (⊓).
+  Global Declare Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓).
+  Global Declare Instance lft_intersect_inj_1 (κ : lft) : Inj eq eq (κ ⊓).
+  Global Declare Instance lft_intersect_inj_2 (κ : lft) : Inj eq eq (⊓ κ).
+  Global Declare Instance lft_intersect_left_id : LeftId eq static meet.
+  Global Declare Instance lft_intersect_right_id : RightId eq static meet.
 
   Global Declare Instance lft_ctx_persistent : Persistent lft_ctx.
   Global Declare Instance lft_dead_persistent κ : Persistent [†κ].
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 15479065691625961afba56a7eca458d52b85470..812e2b6b05ba34348679fb292dc1f75fe63ab900 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -19,7 +19,7 @@ Module Export lft_notation.
 End lft_notation.
 
 Definition static : lft := (∅ : gmultiset _).
-Instance lft_intersect : Meet lft := disj_union.
+Instance lft_intersect : Meet lft := λ κ κ', κ ⊎ κ'.
 
 Inductive bor_state {Lat} :=
   | Bor_in (V : Lat)
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 697b4ec5fa3904c13a1a22ce50d2877c0cb43dab..54f4253a603c01e88e0139dee6fc325e5ec85eb7 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -266,12 +266,12 @@ Qed.
 (** Basic rules about lifetimes  *)
 Instance lft_inhabited : Inhabited lft := _.
 Instance bor_idx_inhabited : Inhabited bor_idx := _.
-Instance lft_intersect_comm : Comm eq lft_intersect := _.
-Instance lft_intersect_assoc : Assoc eq lft_intersect := _.
-Instance lft_intersect_inj_1 κ : Inj eq eq (lft_intersect κ) := _.
-Instance lft_intersect_inj_2 κ : Inj eq eq (λ κ', lft_intersect κ' κ) := _.
-Instance lft_intersect_left_id : LeftId eq static lft_intersect := _.
-Instance lft_intersect_right_id : RightId eq static lft_intersect := _.
+Instance lft_intersect_comm : Comm (A:=lft) eq (⊓) := _.
+Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _.
+Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓) := _.
+Instance lft_intersect_inj_2 κ : Inj eq eq (⊓ κ) := _.
+Instance lft_intersect_left_id : LeftId eq static (⊓) := _.
+Instance lft_intersect_right_id : RightId eq static (⊓) := _.
 
 Lemma lft_tok_sep q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
 Proof. by rewrite /lft_tok -big_sepMS_disj_union. Qed.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 8f19003cbe776eaf07c205e8ead5a156fbb96add..ce48ae79a44e5088fc0005db66bbc2ea630e3f01 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -51,7 +51,7 @@ Section lft_contexts.
     - iDestruct "H" as "[Hq Hq']".
       iDestruct "Hq" as (κ0) "(% & Hq & #?)".
       iDestruct "Hq'" as (κ0') "(% & Hq' & #?)". simpl in *. subst.
-      rewrite (inj ((⊓) (foldr lft_intersect static κs)) κ0' κ0) //.
+      rewrite (inj ((lft_intersect_list κs) ⊓) κ0' κ0) //.
       iExists κ0. by iFrame "∗#".
   Qed.
 
@@ -229,8 +229,8 @@ Section lft_contexts.
     iDestruct "HL" as "[HL1 HL2]". rewrite {2}/llctx_interp /llctx_elt_interp.
     iDestruct (big_sepL_lookup_acc with "HL2") as "[Hκ Hclose]". done.
     iDestruct "Hκ" as (κ0) "(EQ & Htok & #Hend)". simpl. iDestruct "EQ" as %->.
-    iAssert (∃ q', q'.[foldr lft_intersect static κs] ∗
-      (q'.[foldr lft_intersect static κs] ={F}=∗ llctx_interp L (qL / 2)))%I
+    iAssert (∃ q', q'.[lft_intersect_list κs] ∗
+      (q'.[lft_intersect_list κs] ={F}=∗ llctx_interp L (qL / 2)))%I
       with "[> HE HL1]" as "H".
     { move:(qL/2)%Qp=>qL'. clear HL. iClear "Hend".
       iInduction Hκs as [|κ κs Hκ ?] "IH" forall (qL').
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index f5d9cd011b510d67e74870630b55585a9329395b..967f2d59352ae43cab311b9720247eabe20ebb33 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -1191,7 +1191,7 @@ Section arc.
       clear Hclone clone. iIntros (clone) "(Hna & _ & [Hclone _])". rewrite tctx_hasty_val.
       iDestruct "Hs" as "[Hs|Hν']"; last by iDestruct (lft_tok_dead with "Hν Hν'") as "[]".
       iDestruct (lft_intersect_acc with "Hα2 Hν") as (q'') "[Hαν Hclose3]".
-      rewrite -[α ⊓ ν](right_id_L static lft_intersect).
+      rewrite -[α ⊓ ν](right_id_L static (⊓)).
       iApply (type_call_iris _ [α ⊓ ν] (α ⊓ ν) [_] with
               "LFT HE Hna Hαν Hclone [Hl H†]"); [solve_typing| |].
       { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 306d82a01b6cf7c805c4dda7c46a42b4eeab272b..b0ffc6abbbfe7321ff6f6b3342771532e23957d4 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -1094,7 +1094,7 @@ Section code.
       clear clone Hclone. iIntros (clone) "(Hna & _ & Hclone)".
       wp_let. wp_let. rewrite tctx_interp_singleton tctx_hasty_val.
       iDestruct (lft_intersect_acc with "Hα2 Hν") as (q'') "[Hαν Hclose3]".
-      rewrite -[α ⊓ ν](right_id_L static lft_intersect).
+      rewrite -[α ⊓ ν](right_id_L static (⊓)).
       iApply (type_call_iris _ [α ⊓ ν] (α ⊓ ν) [_]
               with "LFT HE Hna Hαν Hclone [H† H↦lr]"); [solve_typing| |].
       { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full_S.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index a257f41ecc518f0510456bd9658cb1571b9bd7fc..4ea4c7c55c94d2fb35a1589a8cd9357cf5327637 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -228,7 +228,7 @@ Section ref_functions.
     iMod (lctx_lft_alive_tok ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
     iDestruct (lft_intersect_acc with "Hα Hν") as (?) "[Hαν Hclose3]".
     iDestruct (lft_intersect_acc with "Hαν Hϝ") as (?) "[Hανϝ Hclose4]".
-    rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ](right_id_L _ lft_intersect).
+    rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ](right_id_L _ (⊓)).
     iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) [_; _]
        with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H†]"); [solve_typing|done| |].
     { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index bd2587ea2c0f96efb52e5dfd748c0bae8aec7551..3f73f40b02f0cee8286897400253d05f6ca6fb3c 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -197,7 +197,7 @@ Section refmut_functions.
     iMod (lctx_lft_alive_tok ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
     iDestruct (lft_intersect_acc with "Hα Hν") as (?) "[Hαν Hclose3]".
     iDestruct (lft_intersect_acc with "Hαν Hϝ") as (?) "[Hανϝ Hclose4]".
-    rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ](right_id_L _ lft_intersect).
+    rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ](right_id_L _ (⊓)).
     iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) [_; _]
             with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H† Hbor]"); [solve_typing|done| |].
     { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.