diff --git a/.gitignore b/.gitignore
index 30ee28f867d2d16d405af4eade8415803f0ba55d..ecdc2641c856c3f94f1daa3e1fb9d99b9c8c9fa1 100644
--- a/.gitignore
+++ b/.gitignore
@@ -10,5 +10,5 @@
 *.bak
 .coq-native/
 iris-enabled
-Makefile.coq
+Makefile.coq*
 opamroot
diff --git a/_CoqProject b/_CoqProject
index 6655f65e692c5824ad66ed962987d2b870bb8056..c447a2bc4de6f5956033a7623b3c76c39d83309d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -56,6 +56,7 @@ theories/typing/lib/fake_shared_box.v
 theories/typing/lib/cell.v
 theories/typing/lib/spawn.v
 theories/typing/lib/join.v
+theories/typing/lib/diverging_static.v
 theories/typing/lib/take_mut.v
 theories/typing/lib/rc/rc.v
 theories/typing/lib/rc/weak.v
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 82200abc1323647c82c559628d7eb1e0cab51bef..e5c15254f70b1af38916ca4e0a67ef4889f1fb26 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -194,4 +194,18 @@ Proof.
   - iApply lft_incl_trans; last iApply IH. (* FIXME: Why does "done" not do this? Looks like "assumption" to me. *)
     iApply lft_intersect_incl_r.
 Qed.
+
+Lemma lft_eternalize E q κ :
+  q.[κ] ={E}=∗ static ⊑ κ.
+Proof.
+  iIntros "Hκ". iMod (inv_alloc lftN _ (∃ q, q.[κ])%I with "[Hκ]") as "#Hnv".
+  { iExists _. done. }
+  iApply lft_incl_intro. iIntros "!> !#". iSplitL.
+  - iIntros (q') "$". iInv lftN as ">Hκ" "Hclose". iDestruct "Hκ" as (q'') "[Hκ1 Hκ2]".
+    iMod ("Hclose" with "[Hκ2]") as "_". { iExists _. done. }
+    iModIntro. iExists _. iFrame. iIntros "_". done.
+  - iIntros "H†". iInv lftN as ">Hκ" "_". iDestruct "Hκ" as (q'') "Hκ".
+    iDestruct (lft_tok_dead with "Hκ H†") as "[]".
+Qed.
+
 End derived.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 3cf52a41af1e07000c1aac5c4c1104685f1e2d51..4c81124ff4f7a64dffd03e0647ad9d9ac6299d56 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -74,16 +74,13 @@ Section lft_contexts.
       elctx_elt_interp (κ1 ⊑ₑ κ2) ∗ elctx_elt_interp (κ2 ⊑ₑ κ1).
   Proof.
     iIntros "#LFT". iDestruct 1 as (κ) "(% & Hκ & _)"; simplify_eq/=.
-    iMod (bor_create _ κ2 (qL).[κ] 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. }
+    iMod (lft_eternalize with "Hκ") as "#Hincl".
     iModIntro. iSplit.
     - iApply lft_incl_trans; iApply lft_intersect_incl_l.
     - 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.
+      + iApply lft_incl_trans; last done. iApply lft_incl_static.
   Qed.
 
   Context (E : elctx) (L : llctx).
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 523c005d4786c686d0bcb8a608465dcb4f1ed107..3d4bfc702d53d650ca1e5b93221ccd02a722fe52 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -19,16 +19,23 @@ Section shr_bor.
   Global Instance shr_bor_wf κ ty `{!TyWf ty} : TyWf (shr_bor κ ty) :=
     { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) κ }.
 
+  Lemma shr_type_incl κ1 κ2 ty1 ty2 :
+    κ2 ⊑ κ1 -∗ type_incl ty1 ty2 -∗ type_incl (shr_bor κ1 ty1) (shr_bor κ2 ty2).
+  Proof.
+    iIntros "#Hκ #[_ [_ Hty]]". iApply type_incl_simple_type. simpl.
+    iIntros "!#" (tid [|[[]|][]]) "H"; try done. iApply "Hty".
+    iApply (ty1.(ty_shr_mono) with "Hκ"). done.
+  Qed.
+
   Global Instance shr_mono E L :
     Proper (flip (lctx_lft_incl E L) ==> subtype E L ==> subtype E L) shr_bor.
   Proof.
-    intros κ1 κ2 Hκ ty1 ty2 Hty. apply subtype_simple_type.
+    intros κ1 κ2 Hκ ty1 ty2 Hty.
     iIntros (?) "/= HL". iDestruct (Hκ with "HL") as "#Hincl".
     iDestruct (Hty with "HL") as "#Hty". iIntros "!# #HE".
-    iIntros (? [|[[]|][]]) "H"; try done. iDestruct ("Hincl" with "HE") as "#Hκ".
-    iApply (ty2.(ty_shr_mono) with "Hκ").
-    iDestruct ("Hty" with "HE") as "(_ & _ & #Hs1)"; [done..|clear Hty].
-    by iApply "Hs1".
+    iApply shr_type_incl.
+    - by iApply "Hincl".
+    - by iApply "Hty".
   Qed.
   Global Instance shr_mono_flip E L :
     Proper (lctx_lft_incl E L ==> flip (subtype E L) ==> flip (subtype E L)) shr_bor.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 2fb6b46e53dc604c5236035f908c747f064c6c4b..21cefb195c8614ce417505f2cdd6e70b58792d49 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -639,16 +639,24 @@ Section subtyping.
     - intros ??? H1 H2. split; etrans; (apply H1 || apply H2).
   Qed.
 
+  Lemma type_incl_simple_type (st1 st2 : simple_type) :
+    □ (∀ tid vl, st1.(st_own) tid vl -∗ st2.(st_own) tid vl) -∗
+    type_incl st1 st2.
+  Proof.
+    iIntros "#Hst". iSplit; first done. iSplit; iAlways.
+    - iIntros. iApply "Hst"; done.
+    - iIntros (???). iDestruct 1 as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
+      by iApply "Hst".
+  Qed.
+
   Lemma subtype_simple_type E L (st1 st2 : simple_type) :
     (∀ qL, llctx_interp L qL -∗ □ (elctx_interp E -∗
        ∀ tid vl, st1.(st_own) tid vl -∗ st2.(st_own) tid vl)) →
     subtype E L st1 st2.
   Proof.
     intros Hst. iIntros (qL) "HL". iDestruct (Hst with "HL") as "#Hst".
-    iClear "∗". iIntros "!# #HE". iSplit; first done. iSplit; iAlways.
-    - iIntros. iApply "Hst"; done.
-    - iIntros (???). iDestruct 1 as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
-      by iApply "Hst".
+    iClear "∗". iIntros "!# #HE". iApply type_incl_simple_type.
+    iIntros "!#" (??) "?". by iApply "Hst".
   Qed.
 
   Lemma subtype_weaken E1 E2 L1 L2 ty1 ty2 :