diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index a2439938202aa5d985f61186901aa5cb16ae5221..ad2291ec71a07fab97cc627319badd15eb7afc68 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -63,6 +63,20 @@ Proof.
   - iIntros "!> !>". iMod "Hclose" as "_". by iApply (bor_fake with "LFT").
 Qed.
 
+Lemma later_bor_static E P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ ▷ P ={E}=∗ &{static} P.
+Proof.
+  iIntros (?) "#LFT HP". iMod (bor_create with "LFT HP") as "[$ _]"; done.
+Qed.
+Lemma bor_static_later E P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{static} P ={E}=∗ ▷ P.
+Proof.
+  iIntros (?) "LFT HP". iMod (bor_acc _ 1%Qp with "LFT HP []") as "[$ _]"; try done.
+  iApply lft_tok_static.
+Qed.
+
 Lemma bor_later_tok E q κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}(▷ P) -∗ q.[κ] ={E}▷=∗ &{κ}P ∗ q.[κ].