diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index c169f25e05c5e05200bba09dbb85b8b42c622d87..4a2eb93179eb71a40e3c25adfedda58e0e26c980 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -16,7 +16,7 @@ Module Export lifetime : lifetime_sig.
   Include creation.
 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 eb1d9569f06d00688644e1b92b0b9b014fa9d52d..773117282efae71db82f51d5e40307d970a41a5e 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -21,7 +21,7 @@ Module Type lifetime_sig.
   (** Definitions *)
   Parameter lft : Type.
   Parameter static : lft.
-  Parameter lft_intersect : lft → lft → lft.
+  Declare Instance lft_intersect : Meet lft.
 
   Parameter lft_ctx : ∀ `{!invG Σ, !lftG Σ}, iProp Σ.
 
@@ -44,7 +44,6 @@ Module Type lifetime_sig.
   Notation "&{ κ , i }" := (idx_bor κ i) (format "&{ κ , i }") : bi_scope.
 
   Infix "⊑" := lft_incl (at level 70) : bi_scope.
-  Infix "⊓" := lft_intersect (at level 40) : stdpp_scope.
 
   Section properties.
   Context `{!invG Σ, !lftG Σ}.
@@ -53,12 +52,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 ede0dc16eb023979a3a9d4bbd1cff202ba1b1783..f2acef14a2b36c11bb0ff4f08c955dba42c87633 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -17,9 +17,7 @@ Module Export lft_notation.
 End lft_notation.
 
 Definition static : lft := (∅ : gmultiset _).
-Definition lft_intersect (κ κ' : lft) : lft := κ ⊎ κ'.
-
-Infix "⊓" := lft_intersect (at level 40) : stdpp_scope.
+Instance lft_intersect : Meet lft := λ κ κ', κ ⊎ κ'.
 
 Inductive bor_state :=
   | Bor_in
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 377a8108b689d949607194147f7f92234fb20633..e3ab4f517363ad4aef0422d6c70983a7beab4c60 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -256,12 +256,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.
@@ -269,7 +269,7 @@ Proof. by rewrite /lft_tok -big_sepMS_disj_union. Qed.
 Lemma lft_dead_or κ1 κ2 : [†κ1] ∨ [†κ2] ⊣⊢ [† κ1 ⊓ κ2].
 Proof.
   rewrite /lft_dead -or_exist. apply exist_proper=> Λ.
-  rewrite -sep_or_r -pure_or. do 2 f_equiv. unfold lft_intersect. set_solver.
+  rewrite -sep_or_r -pure_or. do 2 f_equiv. set_solver.
 Qed.
 
 Lemma lft_tok_dead q κ : q.[κ] -∗ [† κ] -∗ False.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 89829f2ef02d3b306a12ec078eac671f272a38fd..28fa316e225bcd7d14efa5f53bddb466ca6b3cc5 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 *.
-      rewrite (inj (lft_intersect (foldr lft_intersect static κs)) κ0' κ0); last congruence.
+      rewrite (inj ((lft_intersect_list κs) ⊓) κ0' κ0); last congruence.
       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').