diff --git a/_CoqProject b/_CoqProject
index 13d7b219355d675b4293f0e0530a1950503c8f88..f4938067aa076015e602adf7bfd9ec0638652b36 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,13 +1,14 @@
 -Q theories lrust
-theories/lifetime/definitions.v
-theories/lifetime/derived.v
-theories/lifetime/faking.v
-theories/lifetime/creation.v
-theories/lifetime/primitive.v
-theories/lifetime/accessors.v
-theories/lifetime/raw_reborrow.v
-theories/lifetime/borrow.v
-theories/lifetime/reborrow.v
+theories/lifetime/model/definitions.v
+theories/lifetime/model/faking.v
+theories/lifetime/model/creation.v
+theories/lifetime/model/primitive.v
+theories/lifetime/model/accessors.v
+theories/lifetime/model/raw_reborrow.v
+theories/lifetime/model/borrow.v
+theories/lifetime/model/reborrow.v
+theories/lifetime/lifetime_sig.v
+theories/lifetime/lifetime.v
 theories/lifetime/shr_borrow.v
 theories/lifetime/frac_borrow.v
 theories/lifetime/na_borrow.v
diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index 58e72cf04b57985773be26fa1f63d74df063dad9..e402dc73b900954a424559ec860b0ee55769d80f 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -2,6 +2,7 @@ From iris.program_logic Require Export hoare adequacy.
 From iris.algebra Require Import auth.
 From lrust.lang Require Export heap.
 From lrust.lang Require Import proofmode notation.
+Set Default Proof Using "Type".
 
 Class heapPreG Σ := HeapPreG {
   heap_preG_ownP :> ownPPreG lrust_lang Σ;
diff --git a/theories/lang/derived.v b/theories/lang/derived.v
index 00d92652c508146332b832ea9a0e30a97ff035fd..a649ab181f49f124497c91ab00b2110513796fcd 100644
--- a/theories/lang/derived.v
+++ b/theories/lang/derived.v
@@ -1,6 +1,7 @@
 From lrust.lang Require Export lifting.
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
+Set Default Proof Using "Type".
 Import uPred.
 
 (** Define some derived forms, and derived lemmas about them. *)
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 679e3a9bdf438deacae375cc11a6dbb42c8eeb3b..a976118ab31bdad03cfe3f7206d9f50d6fa6c572 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -4,6 +4,7 @@ From iris.algebra Require Import csum excl auth.
 From iris.base_logic Require Import big_op lib.invariants lib.fractional.
 From iris.proofmode Require Export tactics.
 From lrust.lang Require Export lifting.
+Set Default Proof Using "Type".
 Import uPred.
 
 Definition heapN : namespace := nroot .@ "heap".
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index af91c92d719df2a6606c66a7cd9b2fcdba464c61..e770632fbf7d41725a99a49e31628cf26450cfb4 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -1,6 +1,7 @@
 From iris.program_logic Require Export language ectx_language ectxi_language.
 From iris.prelude Require Export strings.
 From iris.prelude Require Import gmap.
+Set Default Proof Using "Type".
 
 Open Scope Z_scope.
 
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index cfd392c0dd3578783a1f185236bdbaecbc0cd047..ede4cd0ff028549c572ffbdda03459cdf979eccd 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -3,6 +3,7 @@ From iris.program_logic Require Import ectx_lifting.
 From lrust.lang Require Export lang.
 From lrust.lang Require Import tactics.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 Import uPred.
 Local Hint Extern 0 (head_reducible _ _) => do_head_step eauto 2.
 
diff --git a/theories/lang/memcpy.v b/theories/lang/memcpy.v
index e65919f1c88aa0815726d06d95d72d67bdf6164a..f11083b0aa8fbbe8a96ef8d9dbdd6ecfc6dbb530 100644
--- a/theories/lang/memcpy.v
+++ b/theories/lang/memcpy.v
@@ -1,6 +1,7 @@
 From iris.base_logic.lib Require Import namespaces.
 From lrust.lang Require Export notation.
 From lrust.lang Require Import heap proofmode.
+Set Default Proof Using "Type".
 
 Definition memcpy : val :=
   rec: "memcpy" ["dst";"len";"src"] :=
diff --git a/theories/lang/new_delete.v b/theories/lang/new_delete.v
index fa541f0f4eccd22afc97e422103213641772a8ee..5b5be8279fabfc7e849d40a5ba712e1df3cb5c90 100644
--- a/theories/lang/new_delete.v
+++ b/theories/lang/new_delete.v
@@ -1,6 +1,7 @@
 From iris.base_logic.lib Require Import namespaces.
 From lrust.lang Require Export notation.
 From lrust.lang Require Import heap proofmode memcpy.
+Set Default Proof Using "Type".
 
 Definition new : val :=
   λ: ["n"],
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index a47399b5d145fdac854bdb8e18f08680fc8f8c12..1caf26f4563ce4fdbd5295e008f31b95488aa489 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -1,4 +1,5 @@
 From lrust.lang Require Export derived.
+Set Default Proof Using "Type".
 
 Coercion LitInt : Z >-> base_lit.
 Coercion LitLoc : loc >-> base_lit.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index fb4d20e89692e4758c5581b997e1d180e304ea3e..44a89ce868a5cfebb040fa5062edd31f52b02c2c 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -2,6 +2,7 @@ From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Export tactics.
 From iris.base_logic Require Import namespaces.
 From lrust.lang Require Export wp_tactics heap.
+Set Default Proof Using "Type".
 Import uPred.
 
 Ltac wp_strip_later ::= iNext.
diff --git a/theories/lang/races.v b/theories/lang/races.v
index dc94392dab068d3bf2d6ee1b193b7322389e2576..c0b8b497e4f64f994cd87c900b3449372c2ee546 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -2,6 +2,7 @@ From iris.prelude Require Import gmap.
 From iris.program_logic Require Export hoare.
 From iris.program_logic Require Import adequacy.
 From lrust.lang Require Import tactics.
+Set Default Proof Using "Type".
 
 Inductive access_kind : Type := ReadAcc | WriteAcc | FreeAcc.
 
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index a622fddae6bdc74629e053f6937d395f8e138820..5767645f97ef27cebbde9e9758b5cd3f58d2cddf 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -1,5 +1,6 @@
 From iris.prelude Require Import fin_maps.
 From lrust.lang Require Export lang.
+Set Default Proof Using "Type".
 
 (** We define an alternative representation of expressions in which the
 embedding of values and closed expressions is explicit. By reification of
diff --git a/theories/lang/wp_tactics.v b/theories/lang/wp_tactics.v
index 12d8f8ca3265b674682c4a0340c1f59d27583d73..f4d6c053e41faa1a9a6143dccf5b077be750ee11 100644
--- a/theories/lang/wp_tactics.v
+++ b/theories/lang/wp_tactics.v
@@ -1,4 +1,5 @@
 From lrust.lang Require Export tactics derived.
+Set Default Proof Using "Type".
 Import uPred.
 
 (** wp-specific helper tactics *)
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 841ac12e746b6eecef9842d0130dc6821f4b715a..e491ea982df64923c1c8e61aee6feda84d808d72 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -2,7 +2,8 @@ From Coq Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import lib.fractional.
 From iris.algebra Require Import frac.
-From lrust.lifetime Require Export shr_borrow .
+From lrust.lifetime Require Export shr_borrow.
+Set Default Proof Using "Type".
 
 Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
 
@@ -127,7 +128,7 @@ Section frac_bor.
   Lemma frac_bor_lft_incl κ κ' q:
     lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
   Proof.
-    iIntros "#LFT#Hbor!#". iSplitR.
+    iIntros "#LFT#Hbor". iApply lft_incl_intro. iAlways. iSplitR.
     - iIntros (q') "Hκ'".
       iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>? Hclose]". done.
       iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
diff --git a/theories/lifetime/derived.v b/theories/lifetime/lifetime.v
similarity index 65%
rename from theories/lifetime/derived.v
rename to theories/lifetime/lifetime.v
index 73b28d1018be895950c35c637f3180878493133d..9ee11aa4c200efc1d625349a64ed0421bec0ec8e 100644
--- a/theories/lifetime/derived.v
+++ b/theories/lifetime/lifetime.v
@@ -1,22 +1,42 @@
-From lrust.lifetime Require Export primitive accessors faking.
-From lrust.lifetime Require Export raw_reborrow.
+From lrust.lifetime Require Export lifetime_sig.
+From lrust.lifetime.model Require definitions primitive accessors faking borrow
+     reborrow creation.
 From iris.proofmode Require Import tactics.
-(* TODO: the name derived makes no sense: reborrow/bor_unnest, which is proven
-in the model, depends on this file. *)
+Set Default Proof Using "Type".
+
+Module Export lifetime : lifetime_sig.
+  Include definitions.
+  Include primitive.
+  Include borrow.
+  Include faking.
+  Include reborrow.
+  Include accessors.
+  Include creation.
+End lifetime.
 
 Section derived.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
-Lemma bor_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
+Lemma bor_acc_cons E q κ P :
   ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
+  lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗
+    ∀ Q, ▷ Q -∗ ▷(▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ} Q ∗ q.[κ].
 Proof.
-  iIntros (?) "#LFT Hb".
-  iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|[H† >_]]"; first done.
-  - iDestruct "H" as "[HΦ Hclose]". iDestruct "HΦ" as (x) "HΦ".
-    iExists x. iApply ("Hclose" with "HΦ"). iIntros "!> ?"; eauto.
-  - iExists inhabitant. by iApply (bor_fake with "LFT").
+  iIntros (?) "#LFT HP Htok".
+  iMod (bor_acc_strong with "LFT HP Htok") as (κ') "(#Hκκ' & $ & Hclose)"; first done.
+  iIntros "!>*HQ HPQ". iMod ("Hclose" with "*HQ [HPQ]") as "[Hb $]".
+  - iNext. iIntros "? _". by iApply "HPQ".
+  - iApply (bor_shorten with "Hκκ' Hb").
+Qed.
+
+Lemma bor_acc E q κ P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
+Proof.
+  iIntros (?) "#LFT HP Htok".
+  iMod (bor_acc_cons with "LFT HP Htok") as "($ & Hclose)"; first done.
+  iIntros "!>HP". iMod ("Hclose" with "*HP []") as "[$ $]"; auto.
 Qed.
 
 Lemma bor_or E κ P Q :
@@ -79,8 +99,9 @@ Qed.
 
 Lemma lft_incl_static κ : (κ ⊑ static)%I.
 Proof.
-  iIntros "!#". iSplitR.
+  iApply lft_incl_intro. iIntros "!#". iSplitR.
   - iIntros (q) "?". iExists 1%Qp. iSplitR. by iApply lft_tok_static. auto.
   - iIntros "Hst". by iDestruct (lft_dead_static with "Hst") as "[]".
 Qed.
 End derived.
+
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
new file mode 100644
index 0000000000000000000000000000000000000000..ea1cb375a425ad8ed01d22e3d815ebf50ef78547
--- /dev/null
+++ b/theories/lifetime/lifetime_sig.v
@@ -0,0 +1,180 @@
+From iris.algebra Require Import csum auth frac gmap agree gset.
+From iris.prelude Require Export gmultiset strings.
+From iris.base_logic.lib Require Export invariants.
+From iris.base_logic.lib Require Import boxes fractional.
+Set Default Proof Using "Type".
+
+Definition lftN : namespace := nroot .@ "lft".
+Definition borN : namespace := lftN .@ "bor".
+Definition inhN : namespace := lftN .@ "inh".
+Definition mgmtN : namespace := lftN .@ "mgmt".
+
+Definition atomic_lft := positive.
+Notation lft := (gmultiset positive).
+Definition static : lft := ∅.
+
+Inductive bor_state :=
+  | Bor_in
+  | Bor_open (q : frac)
+  | Bor_rebor (κ : lft).
+Instance bor_state_eq_dec : EqDecision bor_state.
+Proof. solve_decision. Defined.
+Canonical bor_stateC := leibnizC bor_state.
+
+Record lft_names := LftNames {
+  bor_name : gname;
+  cnt_name : gname;
+  inh_name : gname
+}.
+Instance lft_names_eq_dec : EqDecision lft_names.
+Proof. solve_decision. Defined.
+Canonical lft_namesC := leibnizC lft_names.
+
+Definition lft_stateR := csumR fracR unitR.
+Definition alftUR := gmapUR atomic_lft lft_stateR.
+Definition ilftUR := gmapUR lft (agreeR lft_namesC).
+Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateC)).
+Definition inhUR := gset_disjUR slice_name.
+
+Class lftG Σ := LftG {
+  lft_box :> boxG Σ;
+  alft_inG :> inG Σ (authR alftUR);
+  alft_name : gname;
+  ilft_inG :> inG Σ (authR ilftUR);
+  ilft_name : gname;
+  lft_bor_inG :> inG Σ (authR borUR);
+  lft_cnt_inG :> inG Σ (authR natUR);
+  lft_inh_inG :> inG Σ (authR inhUR);
+}.
+
+Module Type lifetime_sig.
+  (** Definitions *)
+  Parameter lft_ctx : ∀ `{invG, lftG Σ}, iProp Σ.
+
+  Parameter lft_tok : ∀ `{lftG Σ} (q : Qp) (κ : lft), iProp Σ.
+  Parameter lft_dead : ∀ `{lftG Σ} (κ : lft), iProp Σ.
+
+  Parameter lft_incl : ∀ `{invG, lftG Σ} (κ κ' : lft), iProp Σ.
+  Parameter bor : ∀ `{invG, lftG Σ} (κ : lft) (P : iProp Σ), iProp Σ.
+
+  Parameter bor_idx : Type.
+  Parameter idx_bor_own : ∀ `{lftG Σ} (q : frac) (i : bor_idx), iProp Σ.
+  Parameter idx_bor : ∀ `{invG, lftG Σ} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
+  
+  Notation "q .[ κ ]" := (lft_tok q κ)
+      (format "q .[ κ ]", at level 0) : uPred_scope.
+  Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): uPred_scope.
+
+  Notation "&{ κ } P" := (bor κ P)
+    (format "&{ κ }  P", at level 20, right associativity) : uPred_scope.
+  Notation "&{ κ , i } P" := (idx_bor κ i P)
+    (format "&{ κ , i }  P", at level 20, right associativity) : uPred_scope.
+
+  Infix "⊑" := lft_incl (at level 70) : uPred_scope.
+
+  Section properties.
+  Context `{invG, lftG Σ}.
+
+  (** Instances *)
+  Global Declare Instance lft_ctx_persistent : PersistentP lft_ctx.
+  Global Declare Instance lft_dead_persistent κ : PersistentP (lft_dead κ).
+  Global Declare Instance lft_incl_persistent κ κ' : PersistentP (κ ⊑ κ').
+  Global Declare Instance idx_bor_persistent κ i P : PersistentP (idx_bor κ i P).
+
+  Global Declare Instance lft_tok_timeless q κ : TimelessP (lft_tok q κ).
+  Global Declare Instance lft_dead_timeless κ : TimelessP (lft_dead κ).
+  Global Declare Instance idx_bor_own_timeless q i : TimelessP (idx_bor_own q i).
+
+  Global Instance idx_bor_params : Params (@idx_bor) 5.
+  Global Instance bor_params : Params (@bor) 4.
+
+  Global Declare Instance bor_ne κ n : Proper (dist n ==> dist n) (bor κ).
+  Global Declare Instance bor_contractive κ : Contractive (bor κ).
+  Global Declare Instance bor_proper κ : Proper ((≡) ==> (≡)) (bor κ).
+  Global Declare Instance idx_bor_ne κ i n : Proper (dist n ==> dist n) (idx_bor κ i).
+  Global Declare Instance idx_bor_contractive κ i : Contractive (idx_bor κ i).
+  Global Declare Instance idx_bor_proper κ i : Proper ((≡) ==> (≡)) (idx_bor κ i).
+
+  Global Declare Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
+  Global Declare Instance lft_tok_as_fractional κ q :
+    AsFractional q.[κ] (λ q, q.[κ])%I q.
+  Global Declare Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
+  Global Declare Instance idx_bor_own_as_fractional i q :
+    AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
+
+  (** Laws *)
+  Parameter lft_tok_sep : ∀ q κ1 κ2, q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ∪ κ2].
+  Parameter lft_dead_or : ∀ κ1 κ2, [†κ1] ∨ [†κ2] ⊣⊢ [† κ1 ∪ κ2].
+  Parameter lft_tok_dead : ∀ q κ, q.[κ] -∗ [† κ] -∗ False.
+  Parameter lft_tok_static : ∀ q, q.[static]%I.
+  Parameter lft_dead_static : [† static] -∗ False.
+
+  Parameter lft_create : ∀ E, ↑lftN ⊆ E →
+    lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,⊤∖↑lftN}▷=∗ [†κ]).
+  Parameter bor_create : ∀ E κ P,
+    ↑lftN ⊆ E → lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
+  Parameter bor_fake : ∀ E κ P,
+    ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
+
+  Parameter bor_sep : ∀ E κ P Q,
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ} (P ∗ Q) ={E}=∗ &{κ} P ∗ &{κ} Q.
+  Parameter bor_combine : ∀ E κ P Q,
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
+
+  Parameter bor_unfold_idx : ∀ κ P, &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
+  Parameter bor_shorten : ∀ κ κ' P, κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
+  Parameter idx_bor_shorten : ∀ κ κ' i P, κ ⊑ κ' -∗ &{κ',i} P -∗ &{κ,i} P.
+
+  Parameter rebor : ∀ E κ κ' P,
+    ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
+  Parameter bor_unnest : ∀ E κ κ' P,
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ∪ κ'} P.
+
+  Parameter idx_bor_acc : ∀ E q κ i P,
+    ↑lftN ⊆ E →
+    lft_ctx -∗ &{κ,i}P -∗ idx_bor_own 1 i -∗ q.[κ] ={E}=∗
+      ▷ P ∗ (▷ P ={E}=∗ idx_bor_own 1 i ∗ q.[κ]).
+  Parameter idx_bor_atomic_acc : ∀ E q κ i P,
+    ↑lftN ⊆ E →
+    lft_ctx -∗ &{κ,i}P -∗ idx_bor_own q i ={E,E∖↑lftN}=∗
+      (▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ idx_bor_own q i)) ∨
+                ([†κ] ∗ |={E∖↑lftN,E}=> idx_bor_own q i).
+  Parameter bor_acc_strong : ∀ E q κ P,
+    ↑lftN ⊆ E →
+    lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ∃ κ', κ ⊑ κ' ∗ ▷ P ∗
+      ∀ Q, ▷ Q -∗ ▷(▷ Q -∗ [†κ'] ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ'} Q ∗ q.[κ].
+  Parameter bor_acc_atomic_strong : ∀ E κ P,
+    ↑lftN ⊆ E →
+    lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
+      (∃ κ', κ ⊑ κ' ∗ ▷ P ∗
+         ∀ Q, ▷ Q -∗ ▷ (▷ Q -∗ [†κ'] ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
+           ([†κ] ∗ |={E∖↑lftN,E}=> True).
+
+  (* Because Coq's module system is horrible, we have to repeat properties of lft_incl here
+     unless we want to prove them twice (both here and in model.primitive) *)
+  Parameter lft_le_incl : ∀ κ κ', κ' ⊆ κ → (κ ⊑ κ')%I.
+  Parameter lft_incl_refl : ∀ κ, (κ ⊑ κ)%I.
+  Parameter lft_incl_trans : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
+  Parameter lft_incl_glb : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
+  Parameter lft_incl_mono : ∀ κ1 κ1' κ2 κ2',
+    κ1 ⊑ κ1' -∗ κ2 ⊑ κ2' -∗ κ1 ∪ κ2 ⊑ κ1' ∪ κ2'.
+  Parameter lft_incl_acc : ∀ E κ κ' q,
+    ↑lftN ⊆ E → κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
+  Parameter lft_incl_dead : ∀ E κ κ', ↑lftN ⊆ E → κ ⊑ κ' -∗ [†κ'] ={E}=∗ [†κ].
+  Parameter lft_incl_intro : ∀ κ κ',
+    □ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
+                 lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
+        (lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
+  (* Same for some of the derived lemmas. *)
+  Parameter bor_exists : ∀ {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ,
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
+  Parameter bor_acc_atomic_cons : ∀ E κ P,
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
+      (▷ P ∗ ∀ Q, ▷ Q -∗ ▷ (▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ} Q) ∨
+      ([†κ] ∗ |={E∖↑lftN,E}=> True).
+  Parameter bor_acc_atomic : ∀ E κ P,
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
+       (▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ &{κ}P)) ∨ ([†κ] ∗ |={E∖↑lftN,E}=> True).
+
+  End properties.
+End lifetime_sig.
diff --git a/theories/lifetime/accessors.v b/theories/lifetime/model/accessors.v
similarity index 94%
rename from theories/lifetime/accessors.v
rename to theories/lifetime/model/accessors.v
index 14210f73bc4106af113f0cdeb202146fc30440aa..6b53811d3ff680b6877fb60f41b38364598a3d7a 100644
--- a/theories/lifetime/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -3,6 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
+Set Default Proof Using "Type".
 
 Section accessors.
 Context `{invG Σ, lftG Σ}.
@@ -254,18 +255,7 @@ Proof.
       iApply fupd_intro_mask'. solve_ndisj.
 Qed.
 
-Lemma bor_acc_cons E q κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗
-    ∀ Q, ▷ Q -∗ ▷(▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ} Q ∗ q.[κ].
-Proof.
-  iIntros (?) "#LFT HP Htok".
-  iMod (bor_acc_strong with "LFT HP Htok") as (κ') "(#Hκκ' & $ & Hclose)"; first done.
-  iIntros "!>*HQ HPQ". iMod ("Hclose" with "*HQ [HPQ]") as "[Hb $]".
-  - iNext. iIntros "? _". by iApply "HPQ".
-  - iApply (bor_shorten with "Hκκ' Hb").
-Qed.
-
+(* These derived lemmas are needed inside the model. *)
 Lemma bor_acc_atomic_cons E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
@@ -281,15 +271,6 @@ Proof.
   - iRight. by iFrame.
 Qed.
 
-Lemma bor_acc E q κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
-Proof.
-  iIntros (?) "#LFT HP Htok".
-  iMod (bor_acc_cons with "LFT HP Htok") as "($ & Hclose)"; first done.
-  iIntros "!>HP". iMod ("Hclose" with "*HP []") as "[$ $]"; auto.
-Qed.
-
 Lemma bor_acc_atomic E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
@@ -300,4 +281,5 @@ Proof.
   - iLeft. iIntros "!> {$HP} HP". iMod ("Hclose" with "* HP []"); auto.
   - iRight. by iFrame.
 Qed.
+
 End accessors.
diff --git a/theories/lifetime/borrow.v b/theories/lifetime/model/borrow.v
similarity index 99%
rename from theories/lifetime/borrow.v
rename to theories/lifetime/model/borrow.v
index b2bf7ce811f697d4038fc602338087cb393b3dcd..4fba2a91f2ada9046e7430fd3c9887fe32e39711 100644
--- a/theories/lifetime/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -4,6 +4,7 @@ From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 
 Section borrow.
 Context `{invG Σ, lftG Σ}.
@@ -181,4 +182,5 @@ Proof.
       iRight. iSplit; last by auto. iExists _. iFrame. }
     unfold bor. iExists _. iFrame. iApply (lft_incl_glb with "Hκ1 Hκ2").
 Qed.
+
 End borrow.
diff --git a/theories/lifetime/creation.v b/theories/lifetime/model/creation.v
similarity index 99%
rename from theories/lifetime/creation.v
rename to theories/lifetime/model/creation.v
index 5c4cb539aaddee477216f21653a3b4ec9af09581..e731f97ab0cbfbc106d5c67f765bd5a958e7265c 100644
--- a/theories/lifetime/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -4,6 +4,7 @@ From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 
 Section creation.
 Context `{invG Σ, lftG Σ}.
diff --git a/theories/lifetime/definitions.v b/theories/lifetime/model/definitions.v
similarity index 86%
rename from theories/lifetime/definitions.v
rename to theories/lifetime/model/definitions.v
index d98f4dd120fc4f9cfb45fc821bd135a61df8047a..97a5cde305b35e9e2d5d0d30269b4b24a4c9cd8b 100644
--- a/theories/lifetime/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -1,64 +1,20 @@
-From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.prelude Require Export gmultiset strings.
-From iris.base_logic.lib Require Export invariants.
-From iris.base_logic.lib Require Import boxes.
+From iris.algebra Require Import csum auth frac agree gset.
 From iris.base_logic Require Import big_op.
+From iris.base_logic.lib Require Import boxes.
+From lrust.lifetime Require Export lifetime_sig.
+Set Default Proof Using "Type".
 Import uPred.
 
-Definition lftN : namespace := nroot .@ "lft".
-Definition borN : namespace := lftN .@ "bor".
-Definition inhN : namespace := lftN .@ "inh".
-Definition mgmtN : namespace := lftN .@ "mgmt".
-
-Definition atomic_lft := positive.
-Notation lft := (gmultiset positive).
-Definition static : lft := ∅.
-
-Inductive bor_state :=
-  | Bor_in
-  | Bor_open (q : frac)
-  | Bor_rebor (κ : lft).
-Instance bor_state_eq_dec : EqDecision bor_state.
-Proof. solve_decision. Defined.
-Canonical bor_stateC := leibnizC bor_state.
 
 Definition bor_filled (s : bor_state) : bool :=
   match s with Bor_in => true | _ => false end.
 
-Definition lft_stateR := csumR fracR unitR.
 Definition to_lft_stateR (b : bool) : lft_stateR :=
   if b then Cinl 1%Qp else Cinr ().
-
-Record lft_names := LftNames {
-  bor_name : gname;
-  cnt_name : gname;
-  inh_name : gname
-}.
-Instance lft_names_eq_dec : EqDecision lft_names.
-Proof. solve_decision. Defined.
-Canonical lft_namesC := leibnizC lft_names.
-
-Definition alftUR := gmapUR atomic_lft lft_stateR.
 Definition to_alftUR : gmap atomic_lft bool → alftUR := fmap to_lft_stateR.
-
-Definition ilftUR := gmapUR lft (agreeR lft_namesC).
 Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap to_agree.
-
-Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateC)).
 Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,) ∘ to_agree).
 
-Definition inhUR := gset_disjUR slice_name.
-
-Class lftG Σ := LftG {
-  lft_box :> boxG Σ;
-  alft_inG :> inG Σ (authR alftUR);
-  alft_name : gname;
-  ilft_inG :> inG Σ (authR ilftUR);
-  ilft_name : gname;
-  lft_bor_inG :> inG Σ (authR borUR);
-  lft_cnt_inG :> inG Σ (authR natUR);
-  lft_inh_inG :> inG Σ (authR inhUR);
-}.
 
 Section defs.
   Context `{invG Σ, lftG Σ}.
@@ -185,9 +141,9 @@ End defs.
 Instance: Params (@lft_bor_alive) 4.
 Instance: Params (@lft_inh) 5.
 Instance: Params (@lft_vs) 4.
-Instance: Params (@idx_bor) 5.
-Instance: Params (@raw_bor) 4.
-Instance: Params (@bor) 4.
+Instance idx_bor_params : Params (@idx_bor) 5.
+Instance raw_bor_params : Params (@raw_bor) 4.
+Instance bor_params : Params (@bor) 4.
 
 Notation "q .[ κ ]" := (lft_tok q κ)
     (format "q .[ κ ]", at level 0) : uPred_scope.
@@ -200,6 +156,9 @@ Notation "&{ κ , i } P" := (idx_bor κ i P)
 
 Infix "⊑" := lft_incl (at level 70) : uPred_scope.
 
+(* TODO: Making all these things opaque is rather annoying, we should
+   find a way to avoid it, or *at least*, to avoid having to manually unfold
+   this because iDestruct et al don't look through these names any more. *)
 Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
   lft_inh lft_inv_alive lft_vs_inv lft_vs lft_inv_dead lft_inv lft_incl
   idx_bor_own idx_bor raw_bor bor.
@@ -306,8 +265,8 @@ Proof. rewrite /lft_tok. apply _. Qed.
 
 Global Instance lft_dead_persistent κ : PersistentP [†κ].
 Proof. rewrite /lft_dead. apply _. Qed.
-Global Instance lft_dead_timeless κ : PersistentP [†κ].
-Proof. rewrite /lft_tok. apply _. Qed.
+Global Instance lft_dead_timeless κ : TimelessP [†κ].
+Proof. rewrite /lft_dead. apply _. Qed.
 
 Global Instance lft_incl_persistent κ κ' : PersistentP (κ ⊑ κ').
 Proof. rewrite /lft_incl. apply _. Qed.
diff --git a/theories/lifetime/faking.v b/theories/lifetime/model/faking.v
similarity index 98%
rename from theories/lifetime/faking.v
rename to theories/lifetime/model/faking.v
index 7ee7bd10c7a57a2da837c76b5b28dbb6f0db8d0e..07e170e125ae4f9532bc06b80755c289916caee6 100644
--- a/theories/lifetime/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -3,6 +3,7 @@ From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 
 Section faking.
 Context `{invG Σ, lftG Σ}.
@@ -111,8 +112,7 @@ Proof.
 Qed.
 
 Lemma bor_fake E κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
+  ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
 Proof.
   iIntros (?) "#LFT H†". iMod (raw_bor_fake' with "LFT H†"); first done.
   iModIntro. unfold bor. iExists κ. iFrame. iApply lft_incl_refl.
diff --git a/theories/lifetime/primitive.v b/theories/lifetime/model/primitive.v
similarity index 97%
rename from theories/lifetime/primitive.v
rename to theories/lifetime/model/primitive.v
index 235510a1decffa187497b69c678922a794ac62c8..4832b7684bd5539a2f29060bba10e69544b20db0 100644
--- a/theories/lifetime/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -1,8 +1,9 @@
-From lrust.lifetime Require Export definitions.
+From lrust.lifetime.model Require Export definitions.
 From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes fractional.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 Import uPred.
 
 Section primitive.
@@ -352,6 +353,12 @@ Proof.
   iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono; first done. by iApply "H".
 Qed.
 
+Lemma lft_incl_intro κ κ' :
+  □ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
+               lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
+      (lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
+Proof. reflexivity. Qed.
+
 (** Basic rules about borrows *)
 Lemma bor_unfold_idx κ P : &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
 Proof.
@@ -362,7 +369,7 @@ Proof.
     iExists κ'. iFrame. iExists s. by iFrame.
 Qed.
 
-Lemma bor_shorten κ κ' P: κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
+Lemma bor_shorten κ κ' P : κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
 Proof.
   rewrite /bor. iIntros "#Hκκ'". iDestruct 1 as (i) "[#? ?]".
   iExists i. iFrame. by iApply (lft_incl_trans with "Hκκ'").
diff --git a/theories/lifetime/raw_reborrow.v b/theories/lifetime/model/raw_reborrow.v
similarity index 99%
rename from theories/lifetime/raw_reborrow.v
rename to theories/lifetime/model/raw_reborrow.v
index cde623f055df681dbd7a3117a9df0a4d5690b74e..7dbf4a55822586db929a57ced82becf433526a59 100644
--- a/theories/lifetime/raw_reborrow.v
+++ b/theories/lifetime/model/raw_reborrow.v
@@ -4,6 +4,7 @@ From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 
 Section rebor.
 Context `{invG Σ, lftG Σ}.
diff --git a/theories/lifetime/reborrow.v b/theories/lifetime/model/reborrow.v
similarity index 87%
rename from theories/lifetime/reborrow.v
rename to theories/lifetime/model/reborrow.v
index b899064431bdbd8ea3ebe8967bf0020b8a9537e8..59d91f255dc536493ab7b14beb24f237b9ed25ab 100644
--- a/theories/lifetime/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -1,14 +1,27 @@
-From lrust.lifetime Require Export borrow derived.
+From lrust.lifetime Require Export borrow.
 From lrust.lifetime Require Import raw_reborrow accessors.
 From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 
 Section reborrow.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
+(* This lemma has no good place... and reborrowing is where we need it inside the model. *)
+Lemma bor_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
+Proof.
+  iIntros (?) "#LFT Hb".
+  iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|[H† >_]]"; first done.
+  - iDestruct "H" as "[HΦ Hclose]". iDestruct "HΦ" as (x) "HΦ".
+    iExists x. iApply ("Hclose" with "HΦ"). iIntros "!> ?"; eauto.
+  - iExists inhabitant. by iApply (bor_fake with "LFT").
+Qed.
+
 Lemma rebor E κ κ' P :
   ↑lftN ⊆ E →
   lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 16ae3d6943febf8c86dd2cd9592ff1553a70b74b..d61bac2c178ca6a9a5ba1fc4edb0e591cb56c265 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -1,6 +1,7 @@
-From lrust.lifetime Require Export derived.
+From lrust.lifetime Require Export lifetime.
 From iris.base_logic.lib Require Export na_invariants.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 
 Definition na_bor `{invG Σ, lftG Σ, na_invG Σ}
            (κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ) :=
diff --git a/theories/lifetime/shr_borrow.v b/theories/lifetime/shr_borrow.v
index 0df3676db4532358eb5731f343c4bb8ccddc9732..2e1975771a4843bde31af5d3d1360dfbbd7d3b29 100644
--- a/theories/lifetime/shr_borrow.v
+++ b/theories/lifetime/shr_borrow.v
@@ -1,6 +1,7 @@
 From iris.algebra Require Import gmap auth frac.
 From iris.proofmode Require Import tactics.
-From lrust.lifetime Require Export derived.
+From lrust.lifetime Require Export lifetime.
+Set Default Proof Using "Type".
 
 (** Shared bors  *)
 Definition shr_bor `{invG Σ, lftG Σ} κ (P : iProp Σ) :=
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index fa5dc4617549e99cdedcc4a9d60bc7e8e8481c99..c627aa1a8139f06dcaca025c12c005940fa164fa 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -2,6 +2,7 @@ From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs.
+Set Default Proof Using "Type".
 
 Section bool.
   Context `{typeG Σ}.
@@ -20,7 +21,7 @@ Section typing.
   Lemma type_bool_instr (b : Datatypes.bool) E L :
     typed_instruction_ty E L [] #b bool.
   Proof.
-    iIntros (tid qE) "_ _ $ $ $ _". wp_value.
+    iAlways. iIntros (tid qE) "_ _ $ $ $ _". wp_value.
     rewrite tctx_interp_singleton tctx_hasty_val. iExists _. done.
   Qed.
 
@@ -37,7 +38,7 @@ Section typing.
     typed_body E L C T e1 → typed_body E L C T e2 →
     typed_body E L C T (if: p then e1 else e2).
   Proof.
-    iIntros (Hp He1 He2 tid qE) "#HEAP #LFT Htl HE HL HC HT".
+    iIntros (Hp He1 He2) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
     iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "#Hp".
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
     iDestruct "Hown" as (b) "Hv". iDestruct "Hv" as %[=->].
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index f4b4c5eaceb36fca4c9bc34a149a32a7d940c54a..3c3dadd9afbc5ea44f881f4bfb6ca3e503b0a141 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -1,9 +1,9 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
-From lrust.lifetime Require Import reborrow frac_borrow.
 From lrust.lang Require Import heap.
 From lrust.typing Require Export uniq_bor shr_bor own.
 From lrust.typing Require Import lft_contexts type_context programs.
+Set Default Proof Using "Type".
 
 (** The rules for borrowing and derferencing borrowed non-Copy pointers are in
   a separate file so make sure that own.v and uniq_bor.v can be compiled
@@ -48,7 +48,7 @@ Section borrow.
     lctx_lft_alive E L κ →
     typed_instruction_ty E L [p ◁ &uniq{κ} own n ty] (!p) (&uniq{κ} ty).
   Proof.
-    iIntros (Hκ tid eq) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+    iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
     iDestruct "Hown" as (l P) "[[Heq #HPiff] HP]". iDestruct "Heq" as %[=->].
@@ -71,7 +71,7 @@ Section borrow.
     lctx_lft_alive E L κ →
     typed_instruction_ty E L [p ◁ &shr{κ} own n ty] (!p) (&shr{κ} ty).
   Proof.
-    iIntros (Hκ tid eq) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+    iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
     iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
     iDestruct "Hown" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
@@ -88,7 +88,7 @@ Section borrow.
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
     typed_instruction_ty E L [p ◁ &uniq{κ} &uniq{κ'} ty] (!p) (&uniq{κ} ty).
   Proof.
-    iIntros (Hκ Hincl tid eq) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+    iIntros (Hκ Hincl) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
     iPoseProof (Hincl with "[#] [#]") as "Hincl".
     { by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
@@ -118,7 +118,7 @@ Section borrow.
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
     typed_instruction_ty E L [p ◁ &shr{κ} &uniq{κ'} ty] (!p) (&shr{κ} ty).
   Proof.
-    iIntros (Hκ Hincl tid eq) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+    iIntros (Hκ Hincl) "!# * #HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
     iPoseProof (Hincl with "[#] [#]") as "Hincl".
     { by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
     iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 99e45babef51794390b62c7d7d0d8cb942f458cc..3d4398a37aebaa8d4173d8cf9f2f62af2ac65c6e 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -1,8 +1,8 @@
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
-From lrust.lifetime Require Import borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs.
+Set Default Proof Using "Type".
 
 Section typing.
   Context `{typeG Σ}.
@@ -13,7 +13,7 @@ Section typing.
     tctx_incl E L T (T' (list_to_vec args)) →
     typed_body E L C T (k (of_val <$> args)).
   Proof.
-    iIntros (HC Hincl tid qE) "#HEAP #LFT Htl HE HL HC HT".
+    iIntros (HC Hincl) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
     iMod (Hincl with "LFT HE HL HT") as "(HE & HL & HT)".
     iSpecialize ("HC" with "HE * []"); first done.
     rewrite -{3}(vec_to_list_of_list args). iApply ("HC" with "* Htl HL HT").
@@ -26,7 +26,7 @@ Section typing.
     (∀ k, typed_body E L2 (k ◁cont(L1, T') :: C) T (subst' kb k e2)) →
     typed_body E L2 C T (letcont: kb argsb := econt in e2).
   Proof.
-    iIntros (Hc1 Hc2 Hecont He2 tid qE) "#HEAP #LFT Htl HE HL HC HT". iApply wp_let'.
+    iIntros (Hc1 Hc2 Hecont He2) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT". iApply wp_let'.
     { simpl. rewrite decide_left. done. }
     iModIntro. iApply (He2 with "* HEAP LFT Htl HE HL [HC] HT"). clear He2.
     iIntros "HE". iLöb as "IH". iIntros (x) "H".
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index b3fb8b9529f1a1fc19fb3c130ace79a65cf45899..67c01c7d50a62ed3832bc63607165243b16cc4b8 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -1,8 +1,8 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
 From lrust.lang Require Import notation.
-From lrust.lifetime Require Import definitions.
 From lrust.typing Require Import type lft_contexts type_context.
+Set Default Proof Using "Type".
 
 Section cont_context_def.
   Context `{typeG Σ}.
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 2cb0e1b48fb56843a3b439f99e5f5c899a1dd1e5..140ad5f141f7d1ce5f20a1c09e2efa315fbf949d 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -1,5 +1,5 @@
-From lrust.lifetime Require Import definitions.
 From lrust.typing Require Export lft_contexts type bool.
+Set Default Proof Using "Type".
 
 Section fixpoint.
   Context `{typeG Σ}.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index c6391088fef2c203d85ac8ef818528e419ae4ee2..16d30054df04f7742471f8081a2be643d3de55cb 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -1,9 +1,9 @@
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import vector.
-From lrust.lifetime Require Import borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs cont.
+Set Default Proof Using "Type".
 
 Section fn.
   Context `{typeG Σ} {A : Type} {n : nat}.
@@ -12,7 +12,7 @@ Section fn.
           (tys : A → vec type n) (ty : A → type) : type :=
     {| st_own tid vl := (∃ fb kb xb e H,
          ⌜vl = [@RecV fb (kb::xb) e H]⌝ ∗ ⌜length xb = n⌝ ∗
-         □ ▷ ∀ (x : A) (k : val) (xl : vec val (length xb)),
+         ▷ ∀ (x : A) (k : val) (xl : vec val (length xb)),
             typed_body (E x) []
                        [k◁cont([], λ v : vec _ 1, [v!!!0 ◁ ty x])]
                        (zip_with (TCtx_hasty ∘ of_val) xl (tys x))
@@ -30,7 +30,7 @@ Section fn.
   Proof.
     intros ?? Htys ?? Hty. unfold fn. f_equiv. rewrite st_dist_unfold /=.
     f_contractive=>tid vl. unfold typed_body.
-    do 13 f_equiv. f_contractive. do 17 f_equiv.
+    do 12 f_equiv. f_contractive. do 18 f_equiv.
     - rewrite !cctx_interp_singleton /=. do 5 f_equiv.
       rewrite !tctx_interp_singleton /tctx_elt_interp. do 3 f_equiv. apply Hty.
     - rewrite /tctx_interp !big_sepL_zip_with /=. do 3 f_equiv.
@@ -72,8 +72,8 @@ Section typing.
   Proof.
     intros HE Htys Hty. apply subtype_simple_type=>//= _ vl.
     iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
-    iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. iAlways. iNext.
-    rewrite /typed_body. iIntros "* #HEAP _ Htl HE HL HC HT".
+    iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. iNext.
+    rewrite /typed_body. iIntros "* !# * #HEAP _ Htl HE HL HC HT".
     iDestruct (elctx_interp_persist with "HE") as "#HEp".
     iMod (HE with "HE0 HL0 * HE") as (qE') "[HE' Hclose]". done.
     iApply ("Hf" with "* HEAP LFT Htl HE' HL [HC Hclose] [HT]").
@@ -152,7 +152,7 @@ Section typing.
     apply subtype_simple_type=>//= _ vl.
     iIntros "#LFT _ _ Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
     iExists fb, kb, xb, e, _. iSplit. done. iSplit. done.
-    rewrite /typed_body. iAlways. iNext. iIntros "*". iApply "Hf".
+    rewrite /typed_body. iNext. iIntros "*". iApply "Hf".
   Qed.
 
   (* TODO: Define some syntactic sugar for calling and letrec like we do on paper. *)
@@ -163,7 +163,7 @@ Section typing.
                ((p ◁ fn E' tys ty) :: zip_with TCtx_hasty ps (tys x) ++ T)
                (call: p ps → k).
   Proof.
-    iIntros (HE tid qE) "#HEAP #LFT Htl HE HL HC".
+    iIntros (HE) "!# * #HEAP #LFT Htl HE HL HC".
     rewrite tctx_interp_cons tctx_interp_app. iIntros "(Hf & Hargs & HT)".
     wp_bind p. iApply (wp_hasty with "Hf"). iIntros (v) "% Hf".
     iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = k⌝):::
@@ -256,12 +256,12 @@ Section typing.
                    (subst_v (fb :: kb :: argsb) (f ::: k ::: args) e)) →
     typed_instruction_ty E L T (funrec: fb argsb → kb := e) (fn E' tys ty).
   Proof.
-    iIntros (Hc Hbody tid qE) "#HEAP #LFT $ $ $ #HT". iApply wp_value.
+    iIntros (Hc Hbody) "!# * #HEAP #LFT $ $ $ #HT". iApply wp_value.
     { simpl. rewrite decide_left. done. }
     rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
     { simpl. rewrite decide_left. done. }
-    iExists fb, kb, argsb, e, _. iSplit. done. iSplit. done. iAlways. iNext. clear qE.
-    iIntros (x k args tid' qE) "_ _ Htl HE HL HC HT'".
+    iExists fb, kb, argsb, e, _. iSplit. done. iSplit. done. iNext. clear qE.
+    iIntros (x k args) "!#". iIntros (tid' qE) "_ _ Htl HE HL HC HT'".
     iApply (Hbody with "* HEAP LFT Htl HE HL HC").
     rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
     by iApply sendc_change_tid.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 222cf543b0e8ed72c75288f1092d51eebbc6d39b..30ad25cddaae4af527e66fb55ab3325e295b5b0e 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -1,6 +1,7 @@
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 From lrust.typing Require Import bool programs.
+Set Default Proof Using "Type".
 
 Section int.
   Context `{typeG Σ}.
@@ -19,7 +20,7 @@ Section typing.
   Lemma type_int_instr (z : Z) E L :
     typed_instruction_ty E L [] #z int.
   Proof.
-    iIntros (tid qE) "_ _ $ $ $ _". wp_value.
+    iAlways. iIntros (tid qE) "_ _ $ $ $ _". wp_value.
     rewrite tctx_interp_singleton tctx_hasty_val. iExists _. done.
   Qed.
 
@@ -34,7 +35,7 @@ Section typing.
   Lemma type_plus_instr E L p1 p2 :
     typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 + p2) int.
   Proof.
-    iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+    iAlways. iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
     iIntros "[Hp1 Hp2]".
     wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "_ Hown1".
     wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "_ Hown2".
@@ -56,7 +57,7 @@ Section typing.
   Lemma type_minus_instr E L p1 p2 :
     typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 - p2) int.
   Proof.
-    iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+    iAlways. iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
     iIntros "[Hp1 Hp2]".
     wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "_ Hown1".
     wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "_ Hown2".
@@ -78,7 +79,7 @@ Section typing.
   Lemma type_le_instr E L p1 p2 :
     typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 ≤ p2) bool.
   Proof.
-    iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+    iAlways. iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
     iIntros "[Hp1 Hp2]".
     wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "_ Hown1".
     wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "_ Hown2".
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 76e72e949161892315d50aa793dab0b5fb7c3e42..eec88edf6202ba2f77ae69e79052ea0e12812a21 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -1,7 +1,8 @@
 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 Import derived borrow frac_borrow.
+From lrust.lifetime Require Import frac_borrow.
+Set Default Proof Using "Type".
 
 Inductive elctx_elt : Type :=
 | ELCtx_Alive (κ : lft)
diff --git a/theories/typing/own.v b/theories/typing/own.v
index dc065bee07c0c4edb8a6c770040c1b58c4eab8eb..7211456e1e2501f19c35c39be1c1e3af7889bad9 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -1,11 +1,11 @@
 From Coq Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
-From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.lang Require Export new_delete.
 From lrust.lang Require Import memcpy.
 From lrust.typing Require Export type.
 From lrust.typing Require Import uninit type_context programs.
+Set Default Proof Using "Type".
 
 Section own.
   Context `{typeG Σ}.
@@ -158,7 +158,7 @@ Section typing.
   Lemma write_own {E L} ty ty' n :
     ty.(ty_size) = ty'.(ty_size) → typed_write E L (own n ty') ty (own n ty).
   Proof.
-    iIntros (Hsz p tid F qE qL ?) "_ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
+    iIntros (Hsz) "!#". iIntros (p tid F qE qL ?) "_ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
     (* This turns out to be the fastest way to apply a lemma below â–· -- at
     least if we're fine throwing away the premise even though the result
@@ -172,7 +172,7 @@ Section typing.
   Lemma read_own_copy E L ty n :
     Copy ty → typed_read E L (own n ty) ty (own n ty).
   Proof.
-    iIntros (Hsz p tid F qE qL ?) "_ $ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
+    iIntros (Hsz) "!#". iIntros (p tid F qE qL ?) "_ $ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ #Hown]". iModIntro.
     iExists l, _, _. iSplit; first done. iFrame "∗#". iIntros "Hl !>".
     iExists _. iSplit; first done. iFrame "H†". iExists _. by iFrame.
@@ -181,7 +181,7 @@ Section typing.
   Lemma read_own_move E L ty n :
     typed_read E L (own n ty) ty (own n $ uninit ty.(ty_size)).
   Proof.
-    iIntros (p tid F qE qL ?) "_ $ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
+    iAlways. iIntros (p tid F qE qL ?) "_ $ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
     { by iApply ty_size_eq. }
@@ -195,11 +195,11 @@ Section typing.
     let n' := Z.to_nat n in
     typed_instruction_ty E L [] (new [ #n ]%E) (own n' (uninit n')).
   Proof.
-    iIntros (? ? tid q) "#HEAP #LFT $ $ $ _".
+    intros. iAlways. iIntros (tid q) "#HEAP #LFT $ $ $ _".
     iApply (wp_new with "HEAP"); try done. iModIntro.
     iIntros (l vl) "(% & H† & Hlft)". subst. rewrite tctx_interp_singleton tctx_hasty_val.
     iExists _. iSplit; first done. iNext. rewrite freeable_sz_full Z2Nat.id //. iFrame.
-    iExists vl. iFrame. subst n'. by rewrite Nat2Z.id uninit_own.
+    iExists vl. iFrame. by rewrite Nat2Z.id uninit_own.
   Qed.
 
   Lemma type_new E L C T x (n : Z) e :
@@ -214,7 +214,7 @@ Section typing.
     Z.of_nat (ty.(ty_size)) = n →
     typed_instruction E L [p ◁ own (ty.(ty_size)) ty] (delete [ #n; p])%E (λ _, []).
   Proof.
-    iIntros (<- tid eq) "#HEAP #LFT $ $ $ Hp". rewrite tctx_interp_singleton.
+    iIntros (<-) "!#". iIntros (tid eq) "#HEAP #LFT $ $ $ Hp". rewrite tctx_interp_singleton.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
     iDestruct "Hown" as (l) "(Hv & H↦∗: & >H†)". iDestruct "Hv" as %[=->].
     iDestruct "H↦∗:" as (vl) "[>H↦ Hown]". rewrite tctx_interp_nil.
@@ -275,9 +275,17 @@ Section typing.
         - eapply (is_closed_subst []). done. set_solver.
         - by rewrite bool_decide_true.
         - eapply is_closed_subst. done. set_solver. }
-      eapply type_memcpy; try solve_typing.
+      rewrite Nat2Z.id. eapply type_memcpy.
       + apply subst_is_closed; last done. apply is_closed_of_val.
-      + rewrite Nat2Z.id. by apply write_own.
+      + solve_typing.
+      + (* TODO: Doing "eassumption" here shows that unification takes *forever* to fail.
+           I guess that's caused by it trying to unify typed_read and typed_write,
+           but considering that the Iris connectives are all sealed, why does
+           that take so long? *)
+        by eapply (write_own ty (uninit _)).
+      + solve_typing.
+      + done.
+      + done.
   Qed.
 End typing.
 
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 705ae108604ad8cec277027f098453c0701480e0..f91ba5cd359b372c0c74296b445ffed2e38ac75e 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import list.
-From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
+Set Default Proof Using "Type".
 
 Section product.
   Context `{typeG Σ}.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 71cf664038d623b2e91e8400f1f3ad49238c64d6..5911d74ce1341b95edb500cd1eaa125065b933ea 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -1,9 +1,9 @@
 From Coq Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
-From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import type_context lft_contexts product own uniq_bor shr_bor.
+Set Default Proof Using "Type".
 
 Section product_split.
   Context `{typeG Σ}.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index f0901d0b2437cccee6a1708a97c842e3ee072a88..5ba09002b87ce69b7849de69a7e789b36c5acfd9 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -1,8 +1,8 @@
 From iris.base_logic Require Import big_op.
 From lrust.lang Require Export notation.
 From lrust.lang Require Import proofmode memcpy.
-From lrust.lifetime Require Import frac_borrow reborrow borrow creation.
 From lrust.typing Require Export type lft_contexts type_context cont_context.
+Set Default Proof Using "Type".
 
 Section typing.
   Context `{typeG Σ}.
@@ -11,7 +11,7 @@ Section typing.
   (* This is an iProp because it is also used by the function type. *)
   Definition typed_body (E : elctx) (L : llctx) (C : cctx) (T : tctx)
                         (e : expr) : iProp Σ :=
-    (∀ tid qE, heap_ctx -∗ lft_ctx -∗ na_own tid ⊤ -∗
+    (□ ∀ tid qE, heap_ctx -∗ lft_ctx -∗ na_own tid ⊤ -∗
                elctx_interp E qE -∗ llctx_interp L 1 -∗
                (elctx_interp E qE -∗ cctx_interp tid C) -∗ tctx_interp tid T -∗
                WP e {{ _, cont_postcondition }})%I.
@@ -35,7 +35,7 @@ Section typing.
     Proper (flip (cctx_incl E) ==> flip (tctx_incl E L) ==> eq ==> (⊢))
            (typed_body E L).
   Proof.
-    intros C1 C2 HC T1 T2 HT e ? <-. iIntros "H".
+    intros C1 C2 HC T1 T2 HT e ? <-. iIntros "#H !#".
     iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
     iMod (HT with "LFT HE HL HT") as "(HE & HL & HT)".
     iApply ("H" with "HEAP LFT Htl HE HL [HC] HT").
@@ -49,20 +49,20 @@ Section typing.
 
   (** Instruction *)
   Definition typed_instruction (E : elctx) (L : llctx)
-             (T1 : tctx) (e : expr) (T2 : val → tctx) : Prop :=
-    ∀ tid qE, heap_ctx -∗ lft_ctx -∗ na_own tid ⊤ -∗
+             (T1 : tctx) (e : expr) (T2 : val → tctx) : iProp Σ :=
+    (□ ∀ tid qE, heap_ctx -∗ lft_ctx -∗ na_own tid ⊤ -∗
               elctx_interp E qE -∗ llctx_interp L 1 -∗ tctx_interp tid T1 -∗
               WP e {{ v, na_own tid ⊤ ∗ elctx_interp E qE ∗
-                         llctx_interp L 1 ∗ tctx_interp tid (T2 v) }}.
-  Global Arguments typed_instruction _%EL _%LL _%TC _%E _.
+                         llctx_interp L 1 ∗ tctx_interp tid (T2 v) }})%I.
+  Global Arguments typed_instruction _%EL _%LL _%TC _%E _%TC.
 
   (** Writing and Reading **)
-  Definition typed_write (E : elctx) (L : llctx) (ty1 ty ty2 : type) : Prop :=
-    ∀ v tid F qE qL, lftE ∪ (↑lrustN) ⊆ F →
+  Definition typed_write (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
+    (□ ∀ v tid F qE qL, ⌜lftE ∪ (↑lrustN) ⊆ F⌝ →
       lft_ctx -∗ elctx_interp E qE -∗ llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
         ∃ (l : loc) vl, ⌜length vl = ty.(ty_size) ∧ v = #l⌝ ∗ l ↦∗ vl ∗
           (▷ l ↦∗: ty.(ty_own) tid ={F}=∗
-            elctx_interp E qE ∗ llctx_interp L qL ∗ ty2.(ty_own) tid [v]).
+            elctx_interp E qE ∗ llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
   Global Arguments typed_write _%EL _%LL _%T _%T _%T.
 
   (* Technically speaking, we could remvoe the vl quantifiaction here and use
@@ -70,13 +70,13 @@ Section typing.
      make work for some of the provers way harder, since they'd have to show
      that nobody could possibly have changed the vl (because only half the
      fraction was given). So we go with the definition that is easier to prove. *)
-  Definition typed_read (E : elctx) (L : llctx) (ty1 ty ty2 : type) : Prop :=
-    ∀ v tid F qE qL, lftE ∪ (↑lrustN) ⊆ F →
+  Definition typed_read (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
+    (□ ∀ v tid F qE qL, ⌜lftE ∪ (↑lrustN) ⊆ F⌝ →
       lft_ctx -∗ na_own tid F -∗
       elctx_interp E qE -∗ llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
         ∃ (l : loc) vl q, ⌜v = #l⌝ ∗ l ↦∗{q} vl ∗ ▷ ty.(ty_own) tid vl ∗
               (l ↦∗{q} vl ={F}=∗ na_own tid F ∗ elctx_interp E qE ∗
-                              llctx_interp L qL ∗ ty2.(ty_own) tid [v]).
+                              llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
   Global Arguments typed_read _%EL _%LL _%T _%T _%T.
 End typing.
 
@@ -93,7 +93,7 @@ Section typing_rules.
     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".
+    iIntros (He) "!#". iIntros (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").
@@ -108,7 +108,7 @@ Section typing_rules.
     (∀ v : val, typed_body E L C (T2 v ++ T) (subst' xb v e')) →
     typed_body E L C (T1 ++ T) (let: xb := e in e').
   Proof.
-    iIntros (Hc He He' tid qE) "#HEAP #LFT Htl HE HL HC HT". rewrite tctx_interp_app.
+    iIntros (Hc He He') "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT". rewrite tctx_interp_app.
     iDestruct "HT" as "[HT1 HT]". wp_bind e. iApply (wp_wand with "[HE HL HT1 Htl]").
     { iApply (He with "HEAP LFT Htl HE HL HT1"). }
     iIntros (v) "/= (Htl & HE & HL & HT2)". iApply wp_let; first wp_done.
@@ -137,7 +137,7 @@ Section typing_rules.
     (∀ κ, typed_body E ((κ ⊑ κs) :: L) C T e) →
     typed_body E L C T (Newlft ;; e).
   Proof.
-    iIntros (Hc He tid qE) "#HEAP #LFT Htl HE HL HC HT".
+    iIntros (Hc He) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
     iMod (lft_create with "LFT") as (Λ) "[Htk #Hinh]"; first done.
     set (κ' := foldr (∪) static κs). wp_seq.
     iApply (He (κ' ∪ Λ) with "HEAP LFT Htl HE [HL Htk] HC HT").
@@ -151,7 +151,7 @@ Section typing_rules.
     Closed [] e → UnblockTctx κ T1 T2 →
     typed_body E L C T2 e → typed_body E ((κ ⊑ κs) :: L) C T1 (Endlft ;; e).
   Proof.
-    iIntros (Hc Hub He tid qE) "#HEAP #LFT Htl HE". rewrite /llctx_interp big_sepL_cons.
+    iIntros (Hc Hub He) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE". rewrite /llctx_interp big_sepL_cons.
     iIntros "[Hκ HL] HC HT". iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
     iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
     iApply (wp_fupd_step with "Hend"); try done. wp_seq.
@@ -163,11 +163,11 @@ Section typing_rules.
     typed_write E L ty1 ty ty1' →
     typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <- p2) (λ _, [p1 ◁ ty1']%TC).
   Proof.
-    iIntros (Hwrt tid qE) "#HEAP #LFT $ HE HL".
+    iIntros (Hwrt) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL".
     rewrite tctx_interp_cons tctx_interp_singleton. iIntros "[Hp1 Hp2]".
     wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
     wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "_ Hown2".
-    iMod (Hwrt with "* LFT HE HL Hown1") as (l vl) "([% %] & Hl & Hclose)"; first done.
+    iMod (Hwrt with "* [] LFT HE HL Hown1") as (l vl) "([% %] & Hl & Hclose)"; first done.
     subst v1. iAssert (⌜1%nat = ty_size ty⌝%I) with "[#]" as %Hsz.
     { change (1%nat) with (length [v2]). by iApply ty_size_eq. }
     rewrite <-Hsz in *. destruct vl as [|v[|]]; try done.
@@ -190,10 +190,10 @@ Section typing_rules.
     ty.(ty_size) = 1%nat → typed_read E L ty1 ty ty1' →
     typed_instruction E L [p ◁ ty1] (!p) (λ v, [p ◁ ty1'; v ◁ ty]%TC).
   Proof.
-    iIntros (Hsz Hread tid qE) "#HEAP #LFT Htl HE HL Hp".
+    iIntros (Hsz Hread) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL Hp".
     rewrite tctx_interp_singleton. wp_bind p. iApply (wp_hasty with "Hp").
     iIntros (v) "% Hown".
-    iMod (Hread with "* LFT Htl HE HL Hown") as
+    iMod (Hread with "* [] LFT Htl HE HL Hown") as
         (l vl q) "(% & Hl & Hown & Hclose)"; first done.
     subst v. iAssert (▷⌜length vl = 1%nat⌝)%I with "[#]" as ">%".
     { rewrite -Hsz. iApply ty_size_eq. done. }
@@ -217,19 +217,20 @@ Section typing_rules.
 
   Lemma type_memcpy_iris E qE L qL tid ty ty1 ty1' ty2 ty2' (n : Z) p1 p2 :
     Z.of_nat (ty.(ty_size)) = n →
-    typed_write E L ty1 ty ty1' → typed_read E L ty2 ty ty2' →
+    typed_write E L ty1 ty ty1' -∗ typed_read E L ty2 ty ty2' -∗
     {{{ heap_ctx ∗ lft_ctx ∗ na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
         tctx_elt_interp tid (p1 ◁ ty1) ∗ tctx_elt_interp tid (p2 ◁ ty2) }}}
       (p1 <⋯ !{n}p2)
     {{{ RET #(); na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
                  tctx_elt_interp tid (p1 ◁ ty1') ∗ tctx_elt_interp tid (p2 ◁ ty2') }}}.
   Proof.
-    iIntros (<- Hwrt Hread Φ) "(#HEAP & #LFT & Htl & [HE1 HE2] & [HL1 HL2] & [Hp1 Hp2]) HΦ".
+    iIntros (<-) "#Hwrt #Hread !#".
+    iIntros (Φ) "(#HEAP & #LFT & Htl & [HE1 HE2] & [HL1 HL2] & [Hp1 Hp2]) HΦ".
     wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
     wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "% Hown2".
-    iMod (Hwrt with "* LFT HE1 HL1 Hown1")
+    iMod ("Hwrt" with "* [] LFT HE1 HL1 Hown1")
       as (l1 vl1) "([% %] & Hl1 & Hcl1)"; first done.
-    iMod (Hread with "* LFT Htl HE2 HL2 Hown2")
+    iMod ("Hread" with "* [] LFT Htl HE2 HL2 Hown2")
       as (l2 vl2 q2) "(% & Hl2 & Hown2 & Hcl2)"; first done.
     iAssert (▷⌜length vl2 = ty.(ty_size)⌝)%I with "[#]" as ">%".
     { by iApply ty_size_eq. } subst v1 v2. iApply wp_fupd.
@@ -246,8 +247,11 @@ Section typing_rules.
     typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2] (p1 <⋯ !{n}p2)
                       (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
   Proof.
-    iIntros (Hsz Hwrt Hread tid qE) "#HEAP #LFT Htl HE HL HT".
-    iApply (type_memcpy_iris with "[$HEAP $LFT $Htl $HE $HL HT]"); try done.
+    iIntros (Hsz Hwrt Hread) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HT".
+    iApply (type_memcpy_iris with "[] [] * [$HEAP $LFT $Htl $HE $HL HT]"); try done.
+    (* TODO: This is kind of silly, why can't I iApply the assumptions directly? *)
+    { iPoseProof Hwrt as "Hwrt". done. }
+    { iPoseProof Hread as "Hread". done. }
     { by rewrite tctx_interp_cons tctx_interp_singleton. }
     rewrite tctx_interp_cons tctx_interp_singleton. auto.
   Qed.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 83c62f5921c8cef04da7f34e443a3d03bd108bc7..9aef143a737a02ae7a8695e05fd95c5e825240d7 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -1,8 +1,8 @@
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
-From lrust.lifetime Require Import frac_borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import lft_contexts type_context programs.
+Set Default Proof Using "Type".
 
 Section shr_bor.
   Context `{typeG Σ}.
@@ -80,7 +80,7 @@ Section typing.
   Lemma read_shr E L κ ty :
     Copy ty → lctx_lft_alive E L κ → typed_read E L (&shr{κ}ty) ty (&shr{κ}ty).
   Proof.
-    iIntros (Hcopy Halive v tid F qE qL ?) "#LFT Htl HE HL Hown".
+    iIntros (Hcopy Halive) "!#". iIntros (v tid F qE qL ?) "#LFT Htl HE HL Hown".
     iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first set_solver.
     iDestruct "Hown" as (l) "[EQ #Hshr]". iDestruct "EQ" as %[=->].
      assert (↑shrN ⊆ (↑lrustN : coPset)) by solve_ndisj. (* set_solver needs some help. *)
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 6cb8c72a6ea9dfa3ccd4b8c0b1ca5a05e40d2de8..e42e2536f173cfdf302d3d9567d4d70d0a7ed285 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -1,8 +1,8 @@
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import list.
 From iris.base_logic Require Import fractional.
-From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
+Set Default Proof Using "Type".
 
 Section sum.
   Context `{typeG Σ}.
diff --git a/theories/typing/tests/get_x.v b/theories/typing/tests/get_x.v
index 1c7265863212262622923da91a26f57c4c02e005..f76f6aa78d181fa469ffccf8b049e1571496949e 100644
--- a/theories/typing/tests/get_x.v
+++ b/theories/typing/tests/get_x.v
@@ -1,7 +1,7 @@
-From lrust.lifetime Require Import definitions.
 From lrust.lang Require Import new_delete.
 From lrust.typing Require Import programs product product_split own uniq_bor
                     shr_bor int function lft_contexts uninit cont.
+Set Default Proof Using "Type".
 
 Section get_x.
   Context `{typeG Σ}.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 88bb1ddd020c894e1be2c2b4072670a71e2ae203..5e0d853a9f77ecf4da273a27ebc2699859533f59 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -1,8 +1,9 @@
 From iris.base_logic.lib Require Export na_invariants.
 From iris.base_logic Require Import big_op.
 From lrust.lang Require Export proofmode notation.
-From lrust.lifetime Require Import borrow frac_borrow reborrow.
+From lrust.lifetime Require Export frac_borrow.
 From lrust.typing Require Import lft_contexts.
+Set Default Proof Using "Type".
 
 Class typeG Σ := TypeG {
   type_heapG :> heapG Σ;
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index d34c1e132a0aa211d119fbaf6c9d95ce4204ca02..ec4bceff6613164dc1fbccf441b63ddfeb8b9016 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -1,8 +1,8 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
 From lrust.lang Require Import notation.
-From lrust.lifetime Require Import definitions.
 From lrust.typing Require Import type lft_contexts.
+Set Default Proof Using "Type".
 
 Definition path := expr.
 Bind Scope expr_scope with path.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 44e6dfb5a01bb15d4ebe4150a0dccde42b93944f..0e7412d6c3d29bb6accf686d5747f91eaaf4a4d8 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -1,8 +1,8 @@
 From iris.proofmode Require Import tactics.
 From lrust.lang Require Import heap memcpy.
-From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export uninit uniq_bor shr_bor own sum.
 From lrust.typing Require Import lft_contexts type_context programs product.
+Set Default Proof Using "Type".
 
 Section case.
   Context `{typeG Σ}.
@@ -15,7 +15,7 @@ Section case.
       typed_body E L C ((p ◁ own n (sum tyl)) :: T) e) tyl el →
     typed_body E L C ((p ◁ own n (sum tyl)) :: T) (case: !p of el).
   Proof.
-    iIntros (Hel tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
+    iIntros (Hel) "!#". iIntros (tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
     iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hp".
     iDestruct "Hp" as (l) "[EQ [H↦ Hf]]". iDestruct "EQ" as %[=->].
@@ -65,7 +65,7 @@ Section case.
       typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T) e) tyl el →
     typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T) (case: !p of el).
   Proof.
-    iIntros (Halive Hel tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
+    iIntros (Halive Hel) "!#". iIntros (tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
     iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hp".
     iDestruct "Hp" as (l P) "[[EQ HP] Hb]". iDestruct "EQ" as %[=->].
@@ -122,7 +122,7 @@ Section case.
       typed_body E L C ((p ◁ &shr{κ}sum tyl) :: T) e) tyl el →
     typed_body E L C ((p ◁ &shr{κ}sum tyl) :: T) (case: !p of el).
   Proof.
-    iIntros (Halive Hel tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
+    iIntros (Halive Hel) "!#". iIntros (tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
     iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hp".
     iDestruct "Hp" as (l) "[EQ Hl]". iDestruct "EQ" as %[=->].
@@ -156,12 +156,12 @@ Section case.
     typed_write E L ty1 (sum tyl) ty2 →
     typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <-{i} p2) (λ _, [p1 ◁ ty2]%TC).
   Proof.
-    iIntros (Hty Hw ??) "#HEAP #LFT $ HE HL Hp".
+    iIntros (Hty Hw) "!# * #HEAP #LFT $ HE HL Hp".
     rewrite tctx_interp_cons tctx_interp_singleton.
     iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
     iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
     iApply (wp_hasty with "Hp1"). iIntros (v1 Hv1) "Hty1".
-    iMod (Hw with "LFT HE HL Hty1") as (l vl) "(H & H↦ & Hw)"=>//=.
+    iMod (Hw with "* [] LFT HE HL Hty1") as (l vl) "(H & H↦ & Hw)"=>//=.
     destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
     rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
     wp_write. iApply wp_seq. done. iNext. wp_bind p1.
@@ -183,9 +183,9 @@ Section case.
     typed_write E L ty1 (sum tyl) ty2 →
     typed_instruction E L [p ◁ ty1] (p <-{i} ☇) (λ _, [p ◁ ty2]%TC).
   Proof.
-    iIntros (Hty Hw ??) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+    iIntros (Hty Hw) "!# * #HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hty".
-    iMod (Hw with "LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". done.
+    iMod (Hw with "* [] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". done.
     simpl. destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
     rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
     wp_write. rewrite tctx_interp_singleton tctx_hasty_val' //.
@@ -200,18 +200,18 @@ Section case.
     typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2]
                (p1 <⋯{i} !{ty.(ty_size)}p2) (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
   Proof.
-    iIntros (Hty Hw Hr ??) "#HEAP #LFT Htl [HE1 HE2] [HL1 HL2] Hp".
+    iIntros (Hty Hw Hr) "!# * #HEAP #LFT Htl [HE1 HE2] [HL1 HL2] Hp".
     rewrite tctx_interp_cons tctx_interp_singleton.
     iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
     iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
     iApply (wp_hasty with "Hp1"). iIntros (v1 Hv1) "Hty1".
-    iMod (Hw with "LFT HE1 HL1 Hty1") as (l1 vl1) "(H & H↦ & Hw)"=>//=.
+    iMod (Hw with "* [] LFT HE1 HL1 Hty1") as (l1 vl1) "(H & H↦ & Hw)"=>//=.
     destruct vl1 as [|? vl1]; iDestruct "H" as %[[= Hlen] ->].
     rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl1]". wp_write.
     iApply wp_seq. done. iNext. wp_bind p1.
     iApply (wp_wand with "[]"); first by iApply (wp_eval_path). iIntros (? ->).
     wp_op. wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2 Hv2) "Hty2".
-    iMod (Hr with "LFT Htl HE2 HL2 Hty2") as (l2 vl2 q) "(% & H↦2 & Hty & Hr)"=>//=. subst.
+    iMod (Hr with "* [] LFT Htl HE2 HL2 Hty2") as (l2 vl2 q) "(% & H↦2 & Hty & Hr)"=>//=. subst.
     assert (ty.(ty_size) ≤ length vl1).
     { revert i Hty. rewrite Hlen. clear. induction tyl=>//= -[|i] /=.
       - intros [= ->]. lia.
@@ -230,4 +230,4 @@ Section case.
       iExists _. iFrame. rewrite /= drop_length. iPureIntro. lia.
     - iExists _. iFrame.
   Qed.
-End case.
\ No newline at end of file
+End case.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index 6c25430d0fe34861655ee5d894d794874b2f5746..0dbfa1ea03788039d6adc479d934d5938ab8a817 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -1,6 +1,7 @@
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 From lrust.typing Require Import product.
+Set Default Proof Using "Type".
 
 Section uninit.
   Context `{typeG Σ}.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 0bceb2e79f897e06f4a3d1d33e78558b71ad505d..9e553c7394a554aa818e82c24f29b1d6a3963b05 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -1,9 +1,9 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
-From lrust.lifetime Require Import borrow frac_borrow reborrow.
 From lrust.lang Require Import heap.
 From lrust.typing Require Export type.
 From lrust.typing Require Import lft_contexts type_context shr_bor programs.
+Set Default Proof Using "Type".
 
 Section uniq_bor.
   Context `{typeG Σ}.
@@ -224,7 +224,7 @@ Section typing.
   Lemma read_uniq E L κ ty :
     Copy ty → lctx_lft_alive E L κ → typed_read E L (&uniq{κ}ty) ty (&uniq{κ}ty).
   Proof.
-    iIntros (Hcopy Halive v tid F qE qL ?) "#LFT Htl HE HL Hown".
+    iIntros (Hcopy Halive) "!#". iIntros (v tid F qE qL ?) "#LFT Htl HE HL Hown".
     iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first set_solver.
     iDestruct "Hown" as (l P) "[[EQ #HP] H↦]". iDestruct "EQ" as %[=->].
     iMod (bor_iff with "LFT [] H↦") as "H↦". set_solver. by eauto.
@@ -241,7 +241,7 @@ Section typing.
   Lemma write_uniq E L κ ty :
     lctx_lft_alive E L κ → typed_write E L (&uniq{κ}ty) ty (&uniq{κ}ty).
   Proof.
-    iIntros (Halive p tid F qE qL ?) "#LFT HE HL Hown".
+    iIntros (Halive) "!#". iIntros (p tid F qE qL ?) "#LFT HE HL Hown".
     iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
     iDestruct "Hown" as (l P) "[[EQ #HP] H↦]". iDestruct "EQ" as %[=->].
     iMod (bor_iff with "LFT [] H↦") as "H↦". set_solver. by eauto.