diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 0492383bd3dc9d335617be509deefb7d71c5abeb..58d85fb187a1d39928522e449a7de0945330c832 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -148,9 +148,8 @@ Module Type lifetime_sig.
     ↑lftN ⊆ E → κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
   Parameter lft_incl_dead : ∀ E κ κ', ↑lftN ⊆ E → κ ⊑ κ' -∗ [†κ'] ={E}=∗ [†κ].
   Parameter lft_incl_intro : ∀ κ κ',
-    □ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
-                 lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
-        (lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
+    □ ((∀ q, q.[κ] ={↑lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={↑lftN}=∗ q.[κ])) ∗
+        ([†κ'] ={↑lftN}=∗ [†κ])) -∗ κ ⊑ κ'.
 
   End properties.
 
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 5f77eea264f6416e2bf28b5377e72d86789894f2..3751fa3e742ec781e79d01a1aa3903e375e210e5 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -330,9 +330,8 @@ Proof.
 Qed.
 
 Lemma lft_incl_intro κ κ' :
-  □ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
-               lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
-      (lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
+  □ ((∀ q, q.[κ] ={↑lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={↑lftN}=∗ q.[κ])) ∗
+      ([†κ'] ={↑lftN}=∗ [†κ])) -∗ κ ⊑ κ'.
 Proof. reflexivity. Qed.
 
 Lemma lft_intersect_incl_l κ κ': (κ ⊓ κ' ⊑ κ)%I.