diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 664a6c6f444e2abb223ead396bc8708df80ffdc2..70f0b33d1d0e01c236499cb6341b661b52592549 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -46,6 +46,12 @@ Section na_bor.
     iApply (idx_bor_shorten with "Hκκ' H").
   Qed.
 
+  Lemma na_bor_fake E κ: ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &na{κ,tid,N}P.
+  Proof.
+    iIntros (?) "#LFT#H†". iApply (bor_na with ">"). done.
+    by iApply (bor_fake with "LFT H†").
+  Qed.
+
 End na_bor.
 
 Typeclasses Opaque na_bor.