From ec4c621363e9dcd3398ef2d1488f2620b624b443 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 23 Jan 2017 14:08:13 +0100
Subject: [PATCH] Idem for derived kinds of borrows.

---
 theories/lifetime/frac_borrow.v | 104 +++++++++++++++++---------------
 theories/lifetime/na_borrow.v   |  15 +++--
 theories/lifetime/shr_borrow.v  |   6 ++
 theories/typing/unsafe/cell.v   |  36 +++++------
 4 files changed, 86 insertions(+), 75 deletions(-)

diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index c07510ec..d144e141 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -7,14 +7,14 @@ Set Default Proof Using "Type".
 
 Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
 
-Definition frac_bor `{invG Σ, lftG Σ, frac_borG Σ} κ (Φ : Qp → iProp Σ) :=
-  (∃ γ κ', κ ⊑ κ' ∗ &shr{κ'} ∃ q, Φ q ∗ own γ q ∗
+Definition frac_bor `{invG Σ, lftG Σ, frac_borG Σ} κ (φ : Qp → iProp Σ) :=
+  (∃ γ κ', κ ⊑ κ' ∗ &shr{κ'} ∃ q, φ q ∗ own γ q ∗
                        (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ']))%I.
 Notation "&frac{ κ } P" := (frac_bor κ P)
   (format "&frac{ κ }  P", at level 20, right associativity) : uPred_scope.
 
 Section frac_bor.
-  Context `{invG Σ, lftG Σ, frac_borG Σ}.
+  Context `{invG Σ, lftG Σ, frac_borG Σ} (φ : Qp → iProp Σ).
   Implicit Types E : coPset.
 
   Global Instance frac_bor_contractive κ n :
@@ -26,9 +26,17 @@ Section frac_bor.
   Global Instance frac_bor_proper κ :
     Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (frac_bor κ).
   Proof. solve_proper. Qed.
-  Global Instance frac_bor_persistent κ : PersistentP (&frac{κ}Φ) := _.
+  Lemma frac_bor_iff_proper κ φ' :
+    ▷ □ (∀ q, φ q ↔ φ' q) -∗ &frac{κ} φ -∗ &frac{κ} φ'.
+  Proof.
+    iIntros "#Hφφ' H". iDestruct "H" as (γ κ') "[? Hφ]". iExists γ, κ'. iFrame.
+    iApply (shr_bor_iff_proper with "[Hφφ'] Hφ"). iNext. iAlways.
+    iSplit; iIntros "H"; iDestruct "H" as (q) "[H ?]"; iExists q; iFrame; by iApply "Hφφ'".
+  Qed.
 
-  Lemma bor_fracture φ E κ :
+  Global Instance frac_bor_persistent κ : PersistentP (&frac{κ}φ) := _.
+
+  Lemma bor_fracture E κ :
     ↑lftN ⊆ E → lft_ctx -∗ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
   Proof.
     iIntros (?) "#LFT Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
@@ -36,7 +44,7 @@ Section frac_bor.
     - iDestruct "H" as (κ') "(#Hκκ' & Hφ & Hclose)".
       iMod ("Hclose" with "*[-] []") as "Hφ"; last first.
       { iExists γ, κ'. iFrame "#". iApply (bor_share with "Hφ"). done. }
-      { iIntros "!>HΦ H†!>". iNext. iDestruct "HΦ" as (q') "(HΦ & _ & [%|Hκ])". by subst.
+      { iIntros "!>Hφ H†!>". iNext. iDestruct "Hφ" as (q') "(Hφ & _ & [%|Hκ])". by subst.
         iDestruct "Hκ" as (q'') "[_ Hκ]".
         iDestruct (lft_tok_dead with "Hκ H†") as "[]". }
       iExists 1%Qp. iFrame. eauto.
@@ -45,7 +53,7 @@ Section frac_bor.
       iMod (bor_fake with "LFT H†"). done. by iApply bor_share.
   Qed.
 
-  Lemma frac_bor_atomic_acc E κ φ :
+  Lemma frac_bor_atomic_acc E κ :
     ↑lftN ⊆ E →
     lft_ctx -∗ &frac{κ}φ ={E,E∖↑lftN}=∗ (∃ q, ▷ φ q ∗ (▷ φ q ={E∖↑lftN,E}=∗ True))
                                       ∨ [†κ] ∗ |={E∖↑lftN,E}=> True.
@@ -58,85 +66,85 @@ Section frac_bor.
       iApply fupd_intro_mask. set_solver. done.
   Qed.
 
-  Lemma frac_bor_acc' E q κ Φ:
+  Lemma frac_bor_acc' E q κ :
     ↑lftN ⊆ E →
-    lft_ctx -∗ □ (∀ q1 q2, Φ (q1+q2)%Qp ↔ Φ q1 ∗ Φ q2) -∗
-    &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
+    lft_ctx -∗ □ (∀ q1 q2, φ (q1+q2)%Qp ↔ φ q1 ∗ φ q2) -∗
+    &frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={E}=∗ q.[κ]).
   Proof.
-    iIntros (?) "#LFT #HΦ Hfrac Hκ". unfold frac_bor.
+    iIntros (?) "#LFT #Hφ Hfrac Hκ". unfold frac_bor.
     iDestruct "Hfrac" as (γ κ') "#[#Hκκ' Hshr]".
     iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[[Hκ1 Hκ2] Hclose]". done.
     iMod (shr_bor_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
-    iDestruct "H" as (qΦ) "(HΦqΦ & >Hown & Hq)".
-    destruct (Qp_lower_bound (qκ'/2) (qΦ/2)) as (qq & qκ'0 & qΦ0 & Hqκ' & HqΦ).
+    iDestruct "H" as (qφ) "(Hφqφ & >Hown & Hq)".
+    destruct (Qp_lower_bound (qκ'/2) (qφ/2)) as (qq & qκ'0 & qφ0 & Hqκ' & Hqφ).
     iExists qq.
-    iAssert (▷ Φ qq ∗ ▷ Φ (qΦ0 + qΦ / 2))%Qp%I with "[HΦqΦ]" as "[$ HqΦ]".
-    { iNext. rewrite -{1}(Qp_div_2 qΦ) {1}HqΦ. iApply "HΦ". by rewrite assoc. }
-    rewrite -{1}(Qp_div_2 qΦ) {1}HqΦ -assoc {1}Hqκ'.
+    iAssert (▷ φ qq ∗ ▷ φ (qφ0 + qφ / 2))%Qp%I with "[Hφqφ]" as "[$ Hqφ]".
+    { iNext. rewrite -{1}(Qp_div_2 qφ) {1}Hqφ. iApply "Hφ". by rewrite assoc. }
+    rewrite -{1}(Qp_div_2 qφ) {1}Hqφ -assoc {1}Hqκ'.
     iDestruct "Hκ2" as "[Hκq Hκqκ0]". iDestruct "Hown" as "[Hownq Hown]".
-    iMod ("Hclose'" with "[HqΦ Hq Hown Hκq]") as "Hκ1".
+    iMod ("Hclose'" with "[Hqφ Hq Hown Hκq]") as "Hκ1".
     { iNext. iExists _. iFrame. iRight. iDestruct "Hq" as "[%|Hq]".
       - subst. iExists qq. iIntros "{$Hκq}!%".
-        by rewrite (comm _ qΦ0) -assoc (comm _ qΦ0) -HqΦ Qp_div_2.
+        by rewrite (comm _ qφ0) -assoc (comm _ qφ0) -Hqφ Qp_div_2.
       - iDestruct "Hq" as (q') "[% Hq'κ]". iExists (qq + q')%Qp.
-        iIntros "{$Hκq $Hq'κ}!%". by rewrite assoc (comm _ _ qq) assoc -HqΦ Qp_div_2. }
-    clear HqΦ qΦ qΦ0. iIntros "!>HqΦ".
+        iIntros "{$Hκq $Hq'κ}!%". by rewrite assoc (comm _ _ qq) assoc -Hqφ Qp_div_2. }
+    clear Hqφ qφ qφ0. iIntros "!>Hqφ".
     iMod (shr_bor_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
-    iDestruct "H" as (qΦ) "(HΦqΦ & >Hown & >[%|Hq])".
+    iDestruct "H" as (qφ) "(Hφqφ & >Hown & >[%|Hq])".
     { subst. iCombine "Hown" "Hownq" as "Hown".
       by iDestruct (own_valid with "Hown") as %Hval%Qp_not_plus_q_ge_1. }
-    iDestruct "Hq" as (q') "[HqΦq' Hq'κ]". iCombine "Hown" "Hownq" as "Hown".
-    iDestruct (own_valid with "Hown") as %Hval. iDestruct "HqΦq'" as %HqΦq'.
+    iDestruct "Hq" as (q') "[Hqφq' Hq'κ]". iCombine "Hown" "Hownq" as "Hown".
+    iDestruct (own_valid with "Hown") as %Hval. iDestruct "Hqφq'" as %Hqφq'.
     assert (0 < q'-qq ∨ qq = q')%Qc as [Hq'q|<-].
-    { change (qΦ + qq ≤ 1)%Qc in Hval. apply Qp_eq in HqΦq'. simpl in Hval, HqΦq'.
-      rewrite <-HqΦq', <-Qcplus_le_mono_l in Hval. apply Qcle_lt_or_eq in Hval.
+    { change (qφ + qq ≤ 1)%Qc in Hval. apply Qp_eq in Hqφq'. simpl in Hval, Hqφq'.
+      rewrite <-Hqφq', <-Qcplus_le_mono_l in Hval. apply Qcle_lt_or_eq in Hval.
       destruct Hval as [Hval|Hval].
       by left; apply ->Qclt_minus_iff. right; apply Qp_eq, Qc_is_canon. by rewrite Hval. }
     - assert (q' = mk_Qp _ Hq'q + qq)%Qp as ->. { apply Qp_eq. simpl. ring. }
       iDestruct "Hq'κ" as "[Hq'qκ Hqκ]".
-      iMod ("Hclose'" with "[HqΦ HΦqΦ Hown Hq'qκ]") as "Hqκ2".
-      { iNext. iExists (qΦ + qq)%Qp. iFrame. iSplitR "Hq'qκ". by iApply "HΦ"; iFrame.
+      iMod ("Hclose'" with "[Hqφ Hφqφ Hown Hq'qκ]") as "Hqκ2".
+      { iNext. iExists (qφ + qq)%Qp. iFrame. iSplitR "Hq'qκ". by iApply "Hφ"; iFrame.
         iRight. iExists _. iIntros "{$Hq'qκ}!%".
-        revert HqΦq'. rewrite !Qp_eq. move=>/=<-. ring. }
+        revert Hqφq'. rewrite !Qp_eq. move=>/=<-. ring. }
       iApply "Hclose". iFrame. rewrite Hqκ'. by iFrame.
-    - iMod ("Hclose'" with "[HqΦ HΦqΦ Hown]") as "Hqκ2".
-      { iNext. iExists (qΦ ⋅ qq)%Qp. iFrame. iSplitL. by iApply "HΦ"; iFrame. auto. }
+    - iMod ("Hclose'" with "[Hqφ Hφqφ Hown]") as "Hqκ2".
+      { iNext. iExists (qφ ⋅ qq)%Qp. iFrame. iSplitL. by iApply "Hφ"; iFrame. auto. }
       iApply "Hclose". iFrame. rewrite Hqκ'. by iFrame.
   Qed.
 
-  Lemma frac_bor_acc E q κ `{Fractional _ Φ} :
+  Lemma frac_bor_acc E q κ `{Fractional _ φ} :
     ↑lftN ⊆ E →
-    lft_ctx -∗ &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
+    lft_ctx -∗ &frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={E}=∗ q.[κ]).
   Proof.
     iIntros (?) "LFT". iApply (frac_bor_acc' with "LFT"). done.
     iIntros "!#*". rewrite fractional. iSplit; auto.
   Qed.
 
-  Lemma frac_bor_shorten κ κ' Φ: κ ⊑ κ' -∗ &frac{κ'}Φ -∗ &frac{κ}Φ.
+  Lemma frac_bor_shorten κ κ' : κ ⊑ κ' -∗ &frac{κ'}φ -∗ &frac{κ}φ.
   Proof.
     iIntros "Hκκ' H". iDestruct "H" as (γ κ0) "[#H⊑ ?]". iExists γ, κ0. iFrame.
     iApply (lft_incl_trans with "Hκκ' []"). auto.
   Qed.
 
-  Lemma frac_bor_fake E κ Φ:
-    ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &frac{κ}Φ.
+  Lemma frac_bor_fake E κ :
+    ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &frac{κ}φ.
   Proof.
     iIntros (?) "#LFT#H†". iApply (bor_fracture with "LFT >"). done.
     by iApply (bor_fake with "LFT").
   Qed.
-
-  Lemma frac_bor_lft_incl κ κ' q:
-    lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
-  Proof.
-    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.
-    - iIntros "H†'".
-      iMod (frac_bor_atomic_acc with "LFT Hbor") as "[H|[$ $]]". done.
-      iDestruct "H" as (q') "[>Hκ' _]".
-      iDestruct (lft_tok_dead with "Hκ' H†'") as "[]".
-  Qed.
 End frac_bor.
 
+Lemma frac_bor_lft_incl `{invG Σ, lftG Σ, frac_borG Σ} κ κ' q:
+  lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
+Proof.
+  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.
+  - iIntros "H†'".
+    iMod (frac_bor_atomic_acc with "LFT Hbor") as "[H|[$ $]]". done.
+    iDestruct "H" as (q') "[>Hκ' _]".
+    iDestruct (lft_tok_dead with "Hκ' H†'") as "[]".
+Qed.
+
 Typeclasses Opaque frac_bor.
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 3e7940eb..0c59478b 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -14,14 +14,19 @@ Section na_bor.
   Context `{invG Σ, lftG Σ, na_invG Σ}
           (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ).
 
-  Global Instance na_bor_ne κ tid N n :
-    Proper (dist n ==> dist n) (na_bor κ tid N).
+  Global Instance na_bor_ne κ n : Proper (dist n ==> dist n) (na_bor κ tid N).
   Proof. solve_proper. Qed.
-  Global Instance na_bor_contractive κ tid N : Contractive (na_bor κ tid N).
+  Global Instance na_bor_contractive κ : Contractive (na_bor κ tid N).
   Proof. solve_contractive. Qed.
-  Global Instance na_bor_proper κ tid N :
-    Proper ((⊣⊢) ==> (⊣⊢)) (na_bor κ tid N).
+  Global Instance na_bor_proper κ : Proper ((⊣⊢) ==> (⊣⊢)) (na_bor κ tid N).
   Proof. solve_proper. Qed.
+  Lemma na_bor_iff_proper κ P' :
+    ▷ □ (P ↔ P') -∗ &na{κ, tid, N} P -∗ &na{κ, tid, N} P'.
+  Proof.
+    iIntros "HPP' H". iDestruct "H" as (i) "[HP ?]". iExists i. iFrame.
+    iApply (idx_bor_iff_proper with "HPP' HP").
+  Qed.
+
   Global Instance na_bor_persistent κ : PersistentP (&na{κ,tid,N} P) := _.
 
   Lemma bor_na κ E : ↑lftN ⊆ E → &{κ}P ={E}=∗ &na{κ,tid,N}P.
diff --git a/theories/lifetime/shr_borrow.v b/theories/lifetime/shr_borrow.v
index 56a23e07..d4984e20 100644
--- a/theories/lifetime/shr_borrow.v
+++ b/theories/lifetime/shr_borrow.v
@@ -18,6 +18,12 @@ Section shared_bors.
   Proof. solve_contractive. Qed.
   Global Instance shr_bor_proper : Proper ((⊣⊢) ==> (⊣⊢)) (shr_bor κ).
   Proof. solve_proper. Qed.
+  Lemma shr_bor_iff_proper κ P' : ▷ □ (P ↔ P') -∗ &shr{κ} P -∗ &shr{κ} P'.
+  Proof.
+    iIntros "HPP' H". iDestruct "H" as (i) "[HP ?]". iExists i. iFrame.
+    iApply (idx_bor_iff_proper with "HPP' HP").
+  Qed.
+
   Global Instance shr_bor_persistent : PersistentP (&shr{κ} P) := _.
 
   Lemma bor_share E κ : ↑lftN ⊆ E → &{κ}P ={E}=∗ &shr{κ}P.
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index f01a36be..b656ebd8 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -13,16 +13,13 @@ Section cell.
   Program Definition cell (ty : type) :=
     {| ty_size := ty.(ty_size);
        ty_own := ty.(ty_own);
-       ty_shr κ tid l :=
-         (∃ P, ▷ □ (P ↔ l ↦∗: ty.(ty_own) tid) ∗ &na{κ, tid, shrN.@l}P)%I |}.
+       ty_shr κ tid l := (&na{κ, tid, shrN.@l}l ↦∗: ty.(ty_own) tid)%I |}.
   Next Obligation. apply ty_size_eq. Qed.
   Next Obligation.
-    iIntros (ty E κ l tid q ?) "#LFT Hown $". iExists _.
-    iMod (bor_na with "Hown") as "$". set_solver. iIntros "!>!>!#". iSplit; auto.
+    iIntros (ty E κ l tid q ?) "#LFT Hown $". by iApply (bor_na with "Hown").
   Qed.
   Next Obligation.
-    iIntros (ty ?? tid l) "#LFT #H⊑ H". iDestruct "H" as (P) "[??]".
-    iExists _. iFrame. by iApply (na_bor_shorten with "H⊑").
+    iIntros (ty ?? tid l) "#LFT #H⊑ H". by iApply (na_bor_shorten with "H⊑").
   Qed.
 
   Global Instance cell_ne n : Proper (dist n ==> dist n) cell.
@@ -37,9 +34,8 @@ Section cell.
     iDestruct (EQ with "LFT HE HL") as "(% & #Hown & #Hshr)".
     iSplit; [done|iSplit; iIntros "!# * H"].
     - iApply ("Hown" with "H").
-    - iDestruct "H" as (P) "[#HP H]". iExists P. iFrame. iSplit; iNext; iIntros "!# H".
-      + iDestruct ("HP" with "H") as (vl) "[??]". iExists vl. iFrame. by iApply "Hown".
-      + iApply "HP". iDestruct "H" as (vl) "[??]". iExists vl. iFrame. by iApply "Hown".
+    - iApply (na_bor_iff_proper with "[] H"). iSplit; iIntros "!>!# H";
+      iDestruct "H" as (vl) "[??]"; iExists vl; iFrame; by iApply "Hown".
   Qed.
   Lemma cell_mono' E L ty1 ty2 : eqtype E L ty1 ty2 → subtype E L (cell ty1) (cell ty2).
   Proof. eapply cell_mono. Qed.
@@ -53,25 +49,23 @@ Section cell.
   Proof.
     intros ty Hcopy. split; first by intros; simpl; apply _.
     iIntros (κ tid E F l q ??) "#LFT #Hshr Htl Htok". iExists 1%Qp. simpl in *.
-    iDestruct "Hshr" as (P) "[HP Hshr]".
     (* Size 0 needs a special case as we can't keep the thread-local invariant open. *)
     destruct (ty_size ty) as [|sz] eqn:Hsz.
     { iMod (na_bor_acc with "LFT Hshr Htok Htl") as "(Hown & Htl & Hclose)"; [solve_ndisj..|].
-      iDestruct ("HP" with "Hown") as (vl) "[H↦ #Hown]".
+      iDestruct "Hown" as (vl) "[H↦ #Hown]".
       simpl. assert (F ∖ ∅ = F) as -> by set_solver+.
       iDestruct (ty_size_eq with "Hown") as "#>%". rewrite ->Hsz in *.
       iMod ("Hclose" with "[H↦] Htl") as "[$ $]".
-      { iApply "HP". iExists vl. by iFrame. }
+      { iExists vl. by iFrame. }
       iModIntro. iSplitL "".
       { iNext. iExists vl. destruct vl; last done. iFrame "Hown".
         by iApply heap_mapsto_vec_nil. }
       by iIntros "$ _". }
     (* Now we are in the non-0 case. *)
-    iMod (na_bor_acc with "LFT Hshr Htok Htl") as "(H & Htl & Hclose)"; [solve_ndisj..|].
-    iDestruct ("HP" with "H") as "$".
+    iMod (na_bor_acc with "LFT Hshr Htok Htl") as "($ & Htl & Hclose)"; [solve_ndisj..|].
     iDestruct (na_own_acc with "Htl") as "($ & Hclose')"; first by set_solver.
     iIntros "!> Htl Hown". iPoseProof ("Hclose'" with "Htl") as "Htl".
-    iMod ("Hclose" with "[Hown] Htl") as "[$ $]"; last done. by iApply "HP".
+    by iMod ("Hclose" with "Hown Htl") as "[$ $]".
   Qed.
 
   Global Instance cell_send :
@@ -147,22 +141,20 @@ Section typing.
     { (* The core of the proof: Showing that the assignment is safe. *)
       iAlways. iIntros (tid qE) "#HEAP #LFT Htl HE $".
       rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-      iIntros "[Hd Hx]". rewrite {1}/elctx_interp big_opL_singleton /=.
-      destruct d as [[]|]; try iDestruct "Hd" as "[]". iDestruct "Hd" as (P) "[#HP #Hshr]".
+      iIntros "[#Hshr Hx]". rewrite {1}/elctx_interp big_opL_singleton /=.
+      destruct d as [[]|]; try iDestruct "Hshr" as "[]".
       destruct x as [[]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hown >H†]".
       iDestruct "Hown" as (vl') "[>H↦' Hown']".
       iMod (na_bor_acc with "LFT Hshr HE Htl") as "(Hown & Htl & Hclose)"; [solve_ndisj..|].
-      iDestruct ("HP" with "Hown") as (vl) "[>H↦ Hown]".
+      iDestruct ("Hown") as (vl) "[>H↦ Hown]".
       iDestruct (ty_size_eq with "Hown") as "#>%".
       iDestruct (ty_size_eq with "Hown'") as "#>%".
       iApply wp_fupd. iApply (wp_memcpy with "[$HEAP $H↦ $H↦']"); [done..|].
       iNext. iIntros "[H↦ H↦']". rewrite {1}/elctx_interp big_opL_singleton /=.
       iMod ("Hclose" with "[H↦ Hown'] Htl") as "[$ $]".
-      { iApply "HP". iExists vl'. by iFrame. }
+      { iExists vl'. by iFrame. }
       rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //.
-      iSplitR; iModIntro.
-      - iExists _. simpl. eauto.
-      - iFrame. iExists _. iFrame. rewrite uninit_own. auto. }
+      iFrame "∗#". iExists _. iFrame. rewrite uninit_own. auto. }
     intros v. simpl_subst. clear v.
     eapply type_new; [solve_typing..|].
     intros r. simpl_subst.
-- 
GitLab