Use indexed borrow notation.

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.
 

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.