diff --git a/theories/lifetime/shr_borrow.v b/theories/lifetime/shr_borrow.v
index 2db70d36bb3c96688f0741845acef3352b6a6db4..4f5042ef4c7e63c05d7cb32aea0fd79835dd8461 100644
--- a/theories/lifetime/shr_borrow.v
+++ b/theories/lifetime/shr_borrow.v
@@ -4,7 +4,7 @@ From lrust.lifetime Require Export derived.
 
 (** Shared bors  *)
 Definition shr_bor `{invG Σ, lftG Σ} κ (P : iProp Σ) :=
-  (∃ i, idx_bor κ i P ∗ inv lftN (∃ q, idx_bor_own q i))%I.
+  (∃ i, &{κ,i}P ∗ inv lftN (∃ q, idx_bor_own q i))%I.
 Notation "&shr{ κ } P" := (shr_bor κ P)
   (format "&shr{ κ } P", at level 20, right associativity) : uPred_scope.
 
diff --git a/theories/lifetime/tl_borrow.v b/theories/lifetime/tl_borrow.v
index 34d7314179d88a8ae4e0afdde5ce184390f4b439..5770fc4e07a35387bd93af4d9b7b99f5c0e87633 100644
--- a/theories/lifetime/tl_borrow.v
+++ b/theories/lifetime/tl_borrow.v
@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics.
 
 Definition tl_bor `{invG Σ, lftG Σ, thread_localG Σ}
            (κ : lft) (tid : thread_id) (N : namespace) (P : iProp Σ) :=
-  (∃ i, idx_bor κ i P ∗ tl_inv tid N (idx_bor_own 1 i))%I.
+  (∃ i, &{κ,i}P ∗ tl_inv tid N (idx_bor_own 1 i))%I.
 
 Notation "&tl{ κ , tid , N } P" := (tl_bor κ tid N P)
   (format "&tl{ κ , tid , N } P", at level 20, right associativity) : uPred_scope.