diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 04489b3d6cbd34cf41503a7c8c9f1754f29f94f7..6f62322c4a3a20acc1ddfe7fb7126b048cb6374d 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -82,6 +82,17 @@ Section lft_contexts.
       + iApply lft_incl_static.
       + iApply lft_incl_trans; last done. iApply lft_incl_static.
   Qed.
+  Lemma lctx_equalize_lft_static qL κ `{!frac_borG Σ} :
+    lft_ctx -∗ llctx_elt_interp (κ ⊑ₗ []%list) qL ={⊤}=∗
+      elctx_elt_interp (static ⊑ₑ κ).
+  Proof.
+    iIntros "#LFT". iDestruct 1 as (κ') "(% & Hκ & _)"; simplify_eq/=.
+    iMod (lft_eternalize with "Hκ") as "#Hincl".
+    iModIntro.
+    - iApply (lft_incl_glb with "[]"); simpl.
+      + iApply lft_incl_refl.
+      + done.
+  Qed.
 
   Context (E : elctx) (L : llctx).
 
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 6686b012687e1311dd47db18b0e8d9a6844d9912..8291216c4453861fbc2dca404113766f4db68fa1 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -120,6 +120,15 @@ Section typing_rules.
     iApply (He with "LFT [Hκ1 Hκ2 HE] Htl HL HC HT").
     rewrite /elctx_interp /=. by iFrame.
   Qed.
+  Lemma type_equivalize_lft_static E L C T κ e :
+    (⊢ typed_body ((static ⊑ₑ κ) :: E) L C T e) →
+    ⊢ typed_body E ((κ ⊑ₗ []) :: L) C T e.
+  Proof.
+    iIntros (He tid) "#LFT #HE Htl [Hκ HL] HC HT".
+    iMod (lctx_equalize_lft_static with "LFT Hκ") as "Hκ_static".
+    iApply (He with "LFT [Hκ_static HE] Htl HL HC HT").
+    rewrite /elctx_interp /=. by iFrame.
+  Qed.
 
   Lemma type_let' E L T1 T2 (T : tctx) C xb e e' :
     Closed (xb :b: []) e' →