show variant of equalization with the static lifetime

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).
 

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' →