prove lifetime equalizing

theories/typing/lft_contexts.v

 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import fractional.
-From lrust.lifetime Require Export derived.
+From lrust.lifetime Require Import derived borrow frac_borrow.
 
 Inductive elctx_elt : Type :=
 | ELCtx_Alive (κ : lft)
@@ -144,6 +144,24 @@ Section lft_contexts.
     unfold llctx_interp. by iApply (big_sepL_elem_of with "H").
   Qed.
 
+  Lemma lctx_equalize_lft qE qL κ1 κ2 `{!frac_borG Σ} :
+    lft_ctx -∗ llctx_elt_interp (κ1 ⊑ [κ2]%list) qL ={⊤}=∗
+      elctx_elt_interp (κ1 ⊑ κ2) qE ∗ elctx_elt_interp (κ2 ⊑ κ1) qE.
+  Proof.
+    iIntros "#LFT Hκ". rewrite /llctx_elt_interp /=. (* TODO: Why is this unfold necessary? *)
+    iDestruct "Hκ" as (κ) "(% & Hκ & _)".
+    iMod (bor_create _ κ2 with "LFT [Hκ]") as "[Hκ _]"; first done; first by iFrame.
+    iMod (bor_fracture (λ q, (qL * q).[_])%I with "LFT [Hκ]") as "#Hκ"; first done.
+    { rewrite Qp_mult_1_r. done. }
+    iModIntro. subst κ1. iSplit.
+    - iApply lft_le_incl.
+      rewrite <-!gmultiset_union_subseteq_l. done.
+    - iApply (lft_incl_glb with "[]"); first iApply (lft_incl_glb with "[]").
+      + iApply lft_incl_refl.
+      + iApply lft_incl_static.
+      + iApply (frac_bor_lft_incl with "LFT"). done.
+  Qed.
+
   Context (E : elctx) (L : llctx).
 
   (* Lifetime inclusion *)

theories/typing/programs.v

@@ -84,6 +84,22 @@ Notation typed_instruction_ty E L T1 e ty :=
 Section typing_rules.
   Context `{typeG Σ}.
 
+  (* TODO: notation scopes need tuing to avoid the %list here. *)
+  (* TODO: Proof a version of this that substitutes into a compatible context...
+     if we really want to do that. *)
+  Lemma type_equivalize_lft E L C T κ1 κ2 e :
+    typed_body ((κ1 ⊑ κ2) :: (κ2 ⊑ κ1) :: E) L C T e →
+    typed_body E ((κ1 ⊑ [κ2]%list) :: L) C T e.
+  Proof.
+    iIntros (He tid qE) "#HEAP #LFT Htl HE HL HC HT".
+    rewrite /llctx_interp big_sepL_cons. iDestruct "HL" as "[Hκ HL]".
+    iMod (lctx_equalize_lft with "LFT Hκ") as "[Hκ1 Hκ2]".
+    iApply (He with "HEAP LFT Htl [Hκ1 Hκ2 HE] HL [HC] HT").
+    - rewrite /elctx_interp !big_sepL_cons. by iFrame.
+    - rewrite /elctx_interp !big_sepL_cons. iIntros "(_ & _ & HE)".
+      iApply "HC". done.
+  Qed.
+
   Lemma type_let E L T1 T2 (T : tctx) C xb e e' :
     Closed (xb :b: []) e' →
     typed_instruction E L T1 e T2 →