diff --git a/_CoqProject b/_CoqProject
index d91caa8feace58cb818fef3a08e473da6acc56ad..f6fc564e6ad76056b16f1e91495e42207d740723 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -62,7 +62,6 @@ theories/typing/lib/fake_shared.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
@@ -88,3 +87,4 @@ theories/typing/examples/unbox.v
 theories/typing/examples/init_prod.v
 theories/typing/examples/lazy_lft.v
 theories/typing/examples/nonlexical.v
+theories/typing/examples/diverging_static.v
diff --git a/theories/typing/examples/diverging_static.v b/theories/typing/examples/diverging_static.v
new file mode 100644
index 0000000000000000000000000000000000000000..0d23942f2d0669555489a864a56b8541ac52c174
--- /dev/null
+++ b/theories/typing/examples/diverging_static.v
@@ -0,0 +1,40 @@
+From iris.proofmode Require Import tactics.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section diverging_static.
+  Context `{!typeG Σ}.
+
+  (* Show that we can convert any live borrow to 'static with an infinite
+     loop. *)
+  Definition diverging_static_loop (call_once : val) : val :=
+    funrec: <> ["x"; "f"] :=
+      let: "call_once" := call_once in
+      letcall: "ret" := "call_once" ["f"; "x"]%E in
+    withcont: "loop":
+      "loop" []
+    cont: "loop" [] :=
+      "loop" [].
+
+  Lemma diverging_static_loop_type T F call_once
+        `{!TyWf T, !TyWf F} :
+    (* F : FnOnce(&'static T), as witnessed by the impl call_once *)
+    typed_val call_once (fn(∅; F, &shr{static} T) → unit) →
+    typed_val (diverging_static_loop call_once)
+              (fn(∀ α, λ ϝ, ty_outlives_E T static; &shr{α} T, F) → ∅).
+  Proof.
+    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x f. simpl_subst.
+    iApply type_let; [apply Hf|solve_typing|]. iIntros (call); simpl_subst.
+    iApply (type_cont [_] [] (λ r, [(r!!!0%fin:val) ◁ box (unit)])).
+    { iIntros (k). simpl_subst.
+      iApply type_equivalize_lft_static.
+      iApply (type_call [ϝ] ()); solve_typing. }
+    iIntros "!# *". inv_vec args=>r. simpl_subst.
+    iApply (type_cont [] [] (λ r, [])).
+    { iIntros (kloop). simpl_subst. iApply type_jump; solve_typing. }
+    iIntros "!# *". inv_vec args. simpl_subst.
+    iApply type_jump; solve_typing.
+  Qed.
+End diverging_static.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 607a0960a2170debc2e4de36d83b4c625284d640..5d9d512b52878d5b640f205cf9f1016cf8407a40 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -333,13 +333,13 @@ Section typing.
     rewrite tctx_interp_cons tctx_hasty_val. iFrame.
   Qed.
 
-  (* Specialized type_call':  Adapted for use by solve_typing; fixed "list of
-     alive lifetimes" to be the local ones. *)
-  Lemma type_call {A} x E L C T T' T'' p (ps : list path)
+  (* Specialized type_call':  Adapted for use by solve_typing.
+     κs is still expected to be given manually. *)
+  Lemma type_call {A} κs x E L C T T' T'' p (ps : list path)
                         (fp : A → fn_params (length ps)) k :
     p ◁ fn fp ∈ T →
-    Forall (lctx_lft_alive E L) (L.*1) →
-    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> (L.*1)) ++ E) L ((fp x).(fp_E) ϝ)) →
+    Forall (lctx_lft_alive E L) κs →
+    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) L ((fp x).(fp_E) ϝ)) →
     tctx_extract_ctx E L (zip_with TCtx_hasty ps
                                    (box <$> vec_to_list (fp x).(fp_tys))) T T' →
     k ◁cont(L, T'') ∈ C →
diff --git a/theories/typing/lib/diverging_static.v b/theories/typing/lib/diverging_static.v
deleted file mode 100644
index 62fac42d7df3fe3035d9756f58b8c28870287fe6..0000000000000000000000000000000000000000
--- a/theories/typing/lib/diverging_static.v
+++ /dev/null
@@ -1,56 +0,0 @@
-From iris.proofmode Require Import tactics.
-From lrust.typing Require Export type.
-From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
-
-Section diverging_static.
-  Context `{!typeG Σ}.
-
-  (* Show that we can convert any live borrow to 'static with an infinite
-     loop. *)
-  Definition diverging_static_loop (call_once : val) : val :=
-    funrec: <> ["x"; "f"] :=
-      let: "call_once" := call_once in
-      letcall: "ret" := "call_once" ["f"; "x"]%E in
-    withcont: "loop":
-      "loop" []
-    cont: "loop" [] :=
-      "loop" [].
-
-  Lemma diverging_static_loop_type T F call_once
-        `{!TyWf T, !TyWf F} :
-    (* F : FnOnce(&'static T), as witnessed by the impl call_once *)
-    typed_val call_once (fn(∅; F, &shr{static} T) → unit) →
-    typed_val (diverging_static_loop call_once)
-              (fn(∀ α, λ ϝ, ty_outlives_E T static; &shr{α} T, F) → ∅).
-  Proof.
-    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (α ϝ ret arg). inv_vec arg=>x f. simpl_subst.
-    iApply type_let; [apply Hf|solve_typing|]. iIntros (call); simpl_subst.
-    (* Drop to Iris *)
-    iIntros (tid) "#LFT #HE Hna HL Hk (Hcall & Hx & Hf & _)".
-    (* We need a ϝ token to show that we can call F despite it being non-'static. *)
-    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (qϝ) "(Hϝ & HL & _)";
-      [solve_typing..|].
-    iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & _ & _)";
-      [solve_typing..|].
-    iMod (lft_eternalize with "Hα") as "#Hα".
-    iAssert (type_incl (box (&shr{α} T)) (box (&shr{static} T))) as "#[_ [Hincl _]]".
-    { iApply box_type_incl. iNext. iApply shr_type_incl; first done.
-      iApply type_incl_refl. }
-    wp_let. rewrite tctx_hasty_val.
-    iApply (type_call_iris _ [ϝ] () [_; _] with "LFT HE Hna [Hϝ] Hcall [Hx Hf]").
-    - solve_typing.
-    - by rewrite /= (right_id static).
-    - simpl. iFrame. iSplit; last done. rewrite !tctx_hasty_val.
-      iApply "Hincl". done.
-    - iClear "Hα Hincl". iIntros (r) "Htl Hϝ1 Hret". wp_rec.
-      (* Go back to the type system. *)
-      iApply (type_type _ [] _ [] with "[] LFT HE Htl [] Hk [-]"); last first.
-      { rewrite /tctx_interp /=. done. }
-      { rewrite /llctx_interp /=. done. }
-      iApply (type_cont [] [] (λ _, [])).
-      + iIntros (?). simpl_subst. iApply type_jump; solve_typing.
-      + iIntros "!#" (? args). inv_vec args. simpl_subst. iApply type_jump; solve_typing.
-  Qed.
-End diverging_static.