diff --git a/iris b/iris
index ff96075aa1472b1c3b0cfee87cc4ffb06e0f1e2b..513b8d852bf398ca0acfa2e02ed327507c9d2ff0 160000
--- a/iris
+++ b/iris
@@ -1 +1 @@
-Subproject commit ff96075aa1472b1c3b0cfee87cc4ffb06e0f1e2b
+Subproject commit 513b8d852bf398ca0acfa2e02ed327507c9d2ff0
diff --git a/theories/lifetime/borrow.v b/theories/lifetime/borrow.v
index cacfa5ee4bd3936b9a78b62d55deaa8f1dce324d..a690f466837d9ca1d18edd357d4849ceb4f67e3c 100644
--- a/theories/lifetime/borrow.v
+++ b/theories/lifetime/borrow.v
@@ -14,7 +14,7 @@ Lemma bor_fake_internal E κ P :
 Proof.
   iIntros (?) "Hdead". rewrite /lft_bor_dead.
   iDestruct "Hdead" as (B Pinh) "[>Hown Hbox]".
-  iMod (box_insert_empty _ _ _ _ P with "Hbox") as (γ) "(% & Hslice & Hbox)".
+  iMod (box_insert_empty _ P with "Hbox") as (γ) "(% & Hslice & Hbox)".
   iMod (own_bor_update with "Hown") as "Hown".
   { apply auth_update_alloc.
     apply: (alloc_local_update _ _ _ (1%Qp, DecAgree Bor_in)); last done.
@@ -57,10 +57,10 @@ Proof.
     iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
     iDestruct "Halive" as (B) "(HboxB & >HownB & HB)".
     iDestruct "Hinh" as (PE) "[>HownE HboxE]".
-    iMod (box_insert_full _ _ _ _ P with "[$HboxB $HP]")
-      as (γB) "(HBlookup & HsliceB & HboxB)". by solve_ndisj.
+    iMod (box_insert_full with "HP HboxB") as (γB) "(HBlookup & HsliceB & HboxB)".
+      by solve_ndisj.
     rewrite lookup_fmap. iDestruct "HBlookup" as %HBlookup.
-    iMod (box_insert_empty _ _ _ _ P with "HboxE") as (γE) "(% & HsliceE & HboxE)".
+    iMod (box_insert_empty _ P with "HboxE") as (γE) "(% & HsliceE & HboxE)".
     rewrite -(fmap_insert bor_filled _ _ Bor_in) -to_gmap_union_singleton.
     iMod (own_bor_update with "HownB") as "HownB".
     { apply auth_update_alloc.
@@ -99,10 +99,9 @@ Proof.
       rewrite <-elem_of_subseteq_singleton in Hle.
       iMod (own_inh_update with "[HE◯ Hinh]") as "HE●"; [|iApply own_inh_op; by iFrame|].
       { apply auth_update_dealloc, gset_disj_dealloc_local_update. }
-      iMod (box_delete_full with "[$HsliceE $Hbox]") as "[$ Hbox]".
+      iMod (box_delete_full with "HsliceE Hbox") as (Pinh') "($ & _ & Hbox)".
         solve_ndisj. by rewrite lookup_to_gmap_Some.
-      iDestruct "Hbox" as (Pinh') "[_ Hbox]". iApply "Hclose".
-      iExists _, _. iFrame. iNext. iApply "Hclose'". iRight. iFrame "%".
+      iApply "Hclose". iExists _, _. iFrame. iNext. iApply "Hclose'". iRight. iFrame "%".
       iExists _. iFrame. iExists _. iFrame.
       rewrite {1}(union_difference_L {[γE]} ESlices); last set_solver.
       rewrite to_gmap_union_singleton delete_insert // lookup_to_gmap_None. set_solver.
@@ -113,4 +112,14 @@ Proof.
     iFrame. iMod ("Hclose" with "[-]") as "_"; last by auto. iExists _, _. by iFrame.
 Qed.
 
+Lemma bor_sep E κ P Q :
+  ↑lftN ⊆ E →
+  lft_ctx ⊢ &{κ} (P ∗ Q) ={E}=∗ &{κ} P ∗ &{κ} Q.
+Proof.
+Admitted.
+Lemma bor_combine E κ P Q :
+  ↑lftN ⊆ E →
+  lft_ctx ⊢ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
+Proof. Admitted.
+
 End borrow.
\ No newline at end of file
diff --git a/theories/lifetime/creation.v b/theories/lifetime/creation.v
index 1f8c1ee8940f49b6d30f2364f1ceffbd31eb1c0b..8ea552ffac0541f7f4b00a6f9babaa52b5f9c6da 100644
--- a/theories/lifetime/creation.v
+++ b/theories/lifetime/creation.v
@@ -15,7 +15,7 @@ Lemma lft_inh_kill E κ Q :
 Proof.
   rewrite /lft_inh. iIntros (?) "[Hinh HQ]".
   iDestruct "Hinh" as (E') "[Hinh Hbox]".
-  iMod (box_fill_all with "[$Hbox $HQ]") as "?"=>//.
+  iMod (box_fill_all with "Hbox HQ") as "?"=>//.
   rewrite fmap_to_gmap. iModIntro. iExists E'. by iFrame.
 Qed.
 
diff --git a/theories/lifetime/todo.v b/theories/lifetime/todo.v
index 5d60fea4af1e9eee093c6268f1191cfbd7f30ede..ac0911a6fd95aaad8375db1b4ecb91fe4f144249 100644
--- a/theories/lifetime/todo.v
+++ b/theories/lifetime/todo.v
@@ -5,15 +5,6 @@ Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
 (** Basic borrows  *)
-Lemma bor_sep E κ P Q :
-  ↑lftN ⊆ E →
-  lft_ctx ⊢ &{κ} (P ∗ Q) ={E}=∗ &{κ} P ∗ &{κ} Q.
-Proof.
-Admitted.
-Lemma bor_combine E κ P Q :
-  ↑lftN ⊆ E →
-  lft_ctx ⊢ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
-Proof. Admitted.
 Lemma bor_acc_strong E q κ P :
   ↑lftN ⊆ E →
   lft_ctx ⊢ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗