diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 4a2eb93179eb71a40e3c25adfedda58e0e26c980..9d9c54da48414d2a38927a9a4bf9280742616551 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -93,6 +93,13 @@ Proof.
   iMod (bor_exists (A:=bool) with "LFT H") as ([]) "H"; auto.
 Qed.
 
+Lemma bor_iff κ P P' : ▷ □ (P ↔ P') -∗ &{κ}P -∗ &{κ}P'.
+Proof.
+  rewrite !bor_unfold_idx. iIntros "#HP Hbor".
+  iDestruct "Hbor" as (i) "[Hbor Htok]". iExists i. iFrame "Htok".
+  iApply idx_bor_iff; done.
+Qed.
+
 Lemma bor_iff_proper κ P P': ▷ □ (P ↔ P') -∗ □ (&{κ}P ↔ &{κ}P').
 Proof.
   iIntros "#HP !#". iSplit; iIntros "?"; iApply bor_iff; try done.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 10a2939877119948003922343606d5fd397a578c..72b263c8ad4ceec147f5c32917e0571fb7e30df6 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -99,7 +99,6 @@ Module Type lifetime_sig.
   Parameter bor_fake : ∀ E κ P,
     ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
 
-  Parameter bor_iff : ∀ κ P P', ▷ □ (P ↔ P') -∗ &{κ}P -∗ &{κ}P'.
   Parameter bor_shorten : ∀ κ κ' P, κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
 
   Parameter bor_sep : ∀ E κ P Q,