Simplify proofs

theories/lifetime/model/reborrow.v

@@ -60,7 +60,7 @@ Proof.
   { apply auth_update_alloc,
      (alloc_singleton_local_update _ j (1%Qp, to_agree Bor_in)); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HBj. }
-  iModIntro. iExists (P ∗ Pb)%  I. rewrite /Iinv. iFrame "HI Hκ". iSplitL "Hj".
+  iModIntro. iExists (P ∗ Pb)%I. rewrite /Iinv. iFrame "HI Hκ". iSplitL "Hj".
   { iExists j. iFrame. iExists P. rewrite -uPred.iff_refl. auto. }
   iSplitL "Hbox HB● HB".
   { rewrite /lft_bor_alive. iNext. iExists (<[j:=Bor_in]> B).
@@ -123,8 +123,7 @@ Proof.
   iMod (slice_empty _ _ true with "Hs' Hbox") as "[Hidx Hbox]".
     solve_ndisj. by rewrite lookup_fmap EQB.
   iAssert (▷ idx_bor_own 1 (κ, i))%I with "[Hidx]" as ">Hidx"; [by iApply "HP'"|].
-  iDestruct (raw_bor_inI _ _ P with "HI [Hidx]") as %HI;
-    first by rewrite /raw_bor; auto 10 with I.
+  iDestruct (own_bor_auth with "HI [Hidx]") as %HI; [by rewrite /idx_bor_own|].
   iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinvκ Hclose']";
     first by rewrite elem_of_difference elem_of_dom not_elem_of_singleton;
     eauto using strict_ne.

theories/typing/type.v

@@ -134,10 +134,8 @@ Next Obligation.
   iIntros (?? st E κ l tid ??) "#LFT Hmt Hκ".
   iMod (bor_exists with "LFT Hmt") as (vl) "Hmt"; first solve_ndisj.
   iMod (bor_sep with "LFT Hmt") as "[Hmt Hown]"; first solve_ndisj.
-  iMod (bor_persistent with "LFT Hown") as "[Hown|#H†]"; first solve_ndisj.
-  - iFrame "Hκ".
-    iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; by eauto with iFrame.
-  - iExFalso. by iApply (lft_tok_dead with "Hκ").
+  iMod (bor_persistent_tok with "LFT Hown Hκ") as "[Hown $]"; first solve_ndisj.
+  iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; by eauto with iFrame.
 Qed.
 Next Obligation.
   iIntros (?? st κ κ' tid l) "#Hord H".