diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index aed9d929e0d4be7a2b07ed4933dc787af0b548eb..5860f96e64cb5ec85ca7bfa8989cd412f97012aa 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2023-10-14.0.18d22854") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2023-11-06.0.fdf1fcba") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/typing/base.v b/theories/typing/base.v
index 8340847ef27fbff658aea05d73043e7ac36a516b..f81e7fff157cf2ad033a7be8df5582d4f8985f0b 100644
--- a/theories/typing/base.v
+++ b/theories/typing/base.v
@@ -59,15 +59,15 @@ Notation shift_loc_0 := shift_0.
 Notation shift_loc_assoc := shift_lblock_assoc.
 Notation shift_loc_assoc_nat := shift_nat_assoc.
 
-Notation heap_mapsto_agree := own_loc_na_agree.
-
-Notation heap_mapsto_vec := own_loc_na_vec.
-Notation heap_mapsto_vec_nil := own_loc_na_vec_nil.
-Notation heap_mapsto_vec_cons := own_loc_na_vec_cons.
-Notation heap_mapsto_vec_singleton := own_loc_na_vec_singleton.
-Notation heap_mapsto_vec_app := own_loc_na_vec_app.
-Notation heap_mapsto_vec_combine := own_loc_na_vec_combine.
-
-Notation heap_mapsto_pred_wand := own_loc_na_pred_wand.
-Notation heap_mapsto_pred_combine := own_loc_na_pred_combine.
-Notation heap_mapsto_pred_iff_proper := own_loc_na_pred_iff_proper.
+Notation heap_pointsto_agree := own_loc_na_agree.
+
+Notation heap_pointsto_vec := own_loc_na_vec.
+Notation heap_pointsto_vec_nil := own_loc_na_vec_nil.
+Notation heap_pointsto_vec_cons := own_loc_na_vec_cons.
+Notation heap_pointsto_vec_singleton := own_loc_na_vec_singleton.
+Notation heap_pointsto_vec_app := own_loc_na_vec_app.
+Notation heap_pointsto_vec_combine := own_loc_na_vec_combine.
+
+Notation heap_pointsto_pred_wand := own_loc_na_pred_wand.
+Notation heap_pointsto_pred_combine := own_loc_na_pred_combine.
+Notation heap_pointsto_pred_iff_proper := own_loc_na_pred_iff_proper.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 7646e4a1daee5de32804841b0fe37e7d334dc7c9..9d44fb8ea3a26aa601620b868c9a4ff36ceb751c 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -93,7 +93,7 @@ Section borrow.
     wp_apply (wp_hasty with "Hp"); [done|]. iIntros ([[]|]) "_ Hown"; try done.
     iMod (bor_acc_cons with "LFT Hown Htok") as "[H↦ Hclose']". { done. }
     iDestruct "H↦" as ([|[[|l'|]|][]]) "[>H↦ Hown]"; try iDestruct "Hown" as ">[]".
-    iDestruct "Hown" as "[Hown H†]". rewrite heap_mapsto_vec_singleton -wp_fupd. wp_read.
+    iDestruct "Hown" as "[Hown H†]". rewrite heap_pointsto_vec_singleton -wp_fupd. wp_read.
     iMod ("Hclose'" $! (_↦#l' ∗ ⎡freeable_sz n (ty_size ty) l'⎤ ∗ _)%I
           with "[] [H↦ Hown H†]") as "[Hbor Htok]"; last 1 first.
     - iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". { done. }
@@ -102,7 +102,7 @@ Section borrow.
       iDestruct ("HLclose" with "HL") as "$".
       by rewrite tctx_interp_singleton tctx_hasty_val' //=.
     - iIntros "!>(?&?&?)!>". iNext. iExists _.
-      rewrite -heap_mapsto_vec_singleton. iFrame. by iFrame.
+      rewrite -heap_pointsto_vec_singleton. iFrame. by iFrame.
     - iFrame.
   Qed.
 
@@ -157,7 +157,7 @@ Section borrow.
     destruct vl as [|[[]|][]];
       try by iMod (bor_persistent with "LFT Hbor Htok") as "[>[] _]".
     iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". { done. }
-    rewrite heap_mapsto_vec_singleton.
+    rewrite heap_pointsto_vec_singleton.
     iMod (bor_unnest with "LFT Hbor") as "Hbor"; [done|].
     iApply wp_fupd. wp_read.
     iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]"; first by auto.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 539b417f22342ac3002a916f5b24a6480a1d1c8f..8cd1ecb56f26899cddcd6dc5eb3f17994ddf7457 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -165,7 +165,7 @@ Section arc.
     iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
     destruct vl as [|[[|l'|]|][|]];
       try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
-    setoid_rewrite heap_mapsto_vec_singleton.
+    setoid_rewrite heap_pointsto_vec_singleton.
     iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
     iDestruct (monPred_in_intro with "Hb") as (V) "[#Hin Hb]".
     iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
@@ -241,7 +241,7 @@ Section arc.
     - iIntros (tid vl) "Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       iDestruct "Hvl" as "[(Hl1 & Hl2 & H† & Hc) | Hvl]".
       { iLeft. iFrame. iDestruct "Hsz" as %->.
-        iFrame. iApply (heap_mapsto_pred_wand with "Hc"). iApply "Hoincl". }
+        iFrame. iApply (heap_pointsto_pred_wand with "Hc"). iApply "Hoincl". }
       iDestruct "Hvl" as (???? ν t q) "(#Hpersist & Htk & Hν)".
       iRight. iExists _,_,_,_,_,_,_. iFrame "#∗". by iApply arc_persist_type_incl.
     - iIntros "* #Hshr". iDestruct "Hshr" as (l') "[Hfrac Hshr]". iExists l'.
@@ -304,7 +304,7 @@ Section arc.
     iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
     destruct vl as [|[[|l'|]|][|]];
       try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
-    setoid_rewrite heap_mapsto_vec_singleton.
+    setoid_rewrite heap_pointsto_vec_singleton.
     iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
     iDestruct (monPred_in_intro with "Hb") as (V) "[#Hin Hb]".
     iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
@@ -422,11 +422,11 @@ Section arc.
     iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
     iDestruct (ownptr_uninit_own with "Hrcbox")
       as (lrcbox vlrcbox) "(% & Hrcbox↦ & Hrcbox†)". subst rcbox. inv_vec vlrcbox=>???.
-    iDestruct (heap_mapsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
-    iDestruct (heap_mapsto_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
+    iDestruct (heap_pointsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
+    iDestruct (heap_pointsto_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
     rewrite shift_loc_assoc.
     iDestruct (ownptr_uninit_own with "Hrc") as (lrc vlrc) "(% & Hrc↦ & Hrc†)". subst rc.
-    inv_vec vlrc=>?. rewrite heap_mapsto_vec_singleton.
+    inv_vec vlrc=>?. rewrite heap_pointsto_vec_singleton.
     (* All right, we are done preparing our context. Let's get going. *)
     wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write.
     wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
@@ -437,7 +437,7 @@ Section arc.
         with "[] LFT HE Hna HL Hk [>-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
       iSplitL "Hx↦"; first by iExists _; rewrite ->uninit_own; auto.
-      iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame. iLeft.
+      iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame. iLeft.
       rewrite freeable_sz_full_S. iFrame. iExists _. by iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -462,11 +462,11 @@ Section arc.
     iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrc [Hrcbox _]]". rewrite !tctx_hasty_val.
     iDestruct (ownptr_uninit_own with "Hrcbox")
       as (lrcbox vlrcbox) "(% & Hrcbox↦ & Hrcbox†)". subst rcbox. inv_vec vlrcbox=>??? /=.
-    iDestruct (heap_mapsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
-    iDestruct (heap_mapsto_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
+    iDestruct (heap_pointsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
+    iDestruct (heap_pointsto_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
     rewrite shift_loc_assoc.
     iDestruct (ownptr_uninit_own with "Hrc") as (lrc vlrc) "(% & Hrc↦ & Hrc†)". subst rc.
-    inv_vec vlrc=>?. rewrite heap_mapsto_vec_singleton.
+    inv_vec vlrc=>?. rewrite heap_pointsto_vec_singleton.
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lft_create with "LFT") as (ν) "[Hν Hν†]"; first done.
     wp_bind (_ +ₗ _)%E. iSpecialize ("Hν†" with "Hν").
@@ -476,7 +476,7 @@ Section arc.
     iApply (type_type _ _ _ [ #lrc ◁ box (weak ty)]
             with "[] LFT HE Hna HL Hk [>-]"); last first.
     { rewrite tctx_interp_singleton tctx_hasty_val' //=. iFrame.
-      iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+      iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame.
       iMod (create_weak (P1 ν) (P2 lrcbox ty.(ty_size))
             with "Hrcbox↦0 Hrcbox↦1 [-]") as (γi γs γw γsw t q) "[Ha Htok]".
       { rewrite freeable_sz_full_S. iFrame. iExists _. iFrame.
@@ -504,7 +504,7 @@ Section arc.
     iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrcx [#Hrc' [Hx _]]]".
     rewrite !tctx_hasty_val [[rcx]]lock.
     iDestruct (ownptr_uninit_own with "Hx") as (lrc2 vlrc2) "(% & Hx & Hx†)".
-    subst x. inv_vec vlrc2=>?. rewrite heap_mapsto_vec_singleton.
+    subst x. inv_vec vlrc2=>?. rewrite heap_pointsto_vec_singleton.
     destruct rc' as [[|rc'|]|]; try done. simpl of_val.
     iDestruct "Hrc'" as (l') "[Hrc' #Hdelay]".
     (* All right, we are done preparing our context. Let's get going. *)
@@ -523,7 +523,7 @@ Section arc.
     iApply (type_type _ _ _ [ rcx ◁ box (&shr{α}(arc ty)); #lrc2 ◁ box (&shr{α}ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite heap_mapsto_vec_singleton.
+      unlock. iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite heap_pointsto_vec_singleton.
       iFrame "Hx". by iApply ty_shr_mono. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -868,7 +868,7 @@ Section arc.
       rewrite {3}[option]lock. simpl. rewrite -{2 3}lock. (* FIXME: Tried using contextual pattern, did not work. *)
       iDestruct "Hr" as "[Hr ?]". iDestruct "Hr" as ([|d vl]) "[H↦ Hown]";
         first by iDestruct "Hown" as (???) "[>% ?]".
-      rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦1]".
+      rewrite heap_pointsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦1]".
       iDestruct "Hpersist" as "(? & ? & H†)". wp_bind (_ <- _)%E.
       iDestruct "Hdrop" as "[Hν Hdrop]". iSpecialize ("H†" with "Hν").
       iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [done..|set_solver|].
@@ -881,15 +881,15 @@ Section arc.
       iIntros "[? Hrc']". wp_seq.
       wp_apply (drop_fake_spec with "[//] [$Hdrop Hrc' H†] "); [solve_ndisj|..].
       { unfold P2. auto with iFrame. } unlock. iIntros ([]); last first.
-      { iIntros "_". wp_if. unlock. iFrame. iExists (_::_). rewrite heap_mapsto_vec_cons.
+      { iIntros "_". wp_if. unlock. iFrame. iExists (_::_). rewrite heap_pointsto_vec_cons.
         iFrame. iExists 1%nat, _, []. rewrite /= right_id_L Nat.max_0_r.
         auto 10 with iFrame. }
       iIntros "([H† H1] & H2 & H3)". iDestruct "H1" as (vl1) "[H1 Heq]".
       iDestruct "Heq" as %<-. wp_if.
       wp_apply (wp_delete _ _ _ _ (_::_::vl1) with "[H1 H2 H3 H†]"); [done|..].
       { simpl. lia. }
-      { rewrite 2!heap_mapsto_vec_cons shift_loc_assoc. auto with iFrame. }
-      iFrame. iIntros "_". iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame.
+      { rewrite 2!heap_pointsto_vec_cons shift_loc_assoc. auto with iFrame. }
+      iFrame. iIntros "_". iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame.
       iExists 1%nat, _, []. rewrite right_id_L. iFrame. iSplit; [by auto|simpl].
       auto with lia. }
     iIntros (?) "Hr". wp_seq.
@@ -927,7 +927,7 @@ Section arc.
     { destruct b; wp_if=>//. iDestruct "Hdrop" as "((? & H↦) & ? & ?)".
       iDestruct "H↦" as (vl) "[? Heq]". iDestruct "Heq" as %<-.
       wp_apply (wp_delete _ _ _ _ (_::_::vl) with "[-]"); [done|simpl;lia| |done].
-      rewrite !heap_mapsto_vec_cons shift_loc_assoc. iFrame. }
+      rewrite !heap_pointsto_vec_cons shift_loc_assoc. iFrame. }
     iIntros (?) "_". wp_seq.
     (* Finish up the proof. *)
     iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); r ◁ box (uninit 0) ]
@@ -975,13 +975,13 @@ Section arc.
       iDestruct "Hr" as "[Hr >Hfree]". iDestruct "Hr" as (vl0) "[>Hr Hown]".
       iDestruct "Hown" as ">Hlen".
       destruct vl0 as [|? vl0]=>//; iDestruct "Hlen" as %[=Hlen0].
-      rewrite heap_mapsto_vec_cons. iDestruct "Hr" as "[Hr0 Hr1]".
+      rewrite heap_pointsto_vec_cons. iDestruct "Hr" as "[Hr0 Hr1]".
       iDestruct "Hpersist" as "(Ha & _ & H†)". wp_bind (_ <- _)%E.
       iSpecialize ("H†" with "Hν").
       iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [done..|set_solver+|].
       iApply (wp_mask_mono _ (↑histN)); [set_solver+|].
       wp_write. iIntros "(#Hν & Hown & H†) !>". wp_seq. wp_op. wp_op.
-      rewrite -(firstn_skipn ty.(ty_size) vl0) heap_mapsto_vec_app.
+      rewrite -(firstn_skipn ty.(ty_size) vl0) heap_pointsto_vec_app.
       iDestruct "Hr1" as "[Hr1 Hr2]". iDestruct "Hown" as (vl) "[Hrc' Hown]".
       iDestruct (ty_size_eq with "Hown") as %Hlen.
       wp_apply (wp_memcpy with "[$Hr1 $Hrc']"); [done|..];
@@ -994,14 +994,14 @@ Section arc.
       { destruct b; wp_if=>//. iDestruct "Hdrop" as "((? & H↦) & ? & ?)".
         iDestruct "H↦" as (vl') "[? Heq]". iDestruct "Heq" as %<-.
         wp_apply (wp_delete _ _ _ _ (_::_::vl') with "[-]"); [done|simpl; lia| |done].
-        rewrite !heap_mapsto_vec_cons shift_loc_assoc. iFrame. }
+        rewrite !heap_pointsto_vec_cons shift_loc_assoc. iFrame. }
       iIntros (?) "_". wp_seq.
       iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); #r ◁ box (Σ[ ty; arc ty ]) ]
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock.
         iFrame. iCombine "Hr1" "Hr2" as "Hr1". iCombine "Hr0" "Hr1" as "Hr".
-        rewrite -[in _ +â‚— ty.(ty_size)]Hlen -heap_mapsto_vec_app
-                -heap_mapsto_vec_cons tctx_hasty_val' //. iFrame. iExists _. iFrame.
+        rewrite -[in _ +â‚— ty.(ty_size)]Hlen -heap_pointsto_vec_app
+                -heap_pointsto_vec_cons tctx_hasty_val' //. iFrame. iExists _. iFrame.
         iExists O, _, _. iSplit; first by auto. iFrame. iIntros "!> !% /=".
         rewrite app_length drop_length. lia. }
       iApply type_delete; [solve_typing..|].
@@ -1046,7 +1046,7 @@ Section arc.
     iMod (bor_sep with "LFT Hrc'") as "[Hrc'↦ Hrc]"=>//.
     destruct rcvl as [|[[|rc|]|][|]]; try by
       iMod (bor_persistent with "LFT Hrc Hα") as "[>[] ?]".
-    rewrite heap_mapsto_vec_singleton.
+    rewrite heap_pointsto_vec_singleton.
     iMod (bor_acc with "LFT Hrc'↦ Hα") as "[Hrc'↦ Hclose2]"=>//. wp_read.
     iMod ("Hclose2" with "Hrc'↦") as "[_ Hα]".
     iMod (bor_acc_cons with "LFT Hrc Hα") as "[Hrc Hclose2]"=>//. wp_let.
@@ -1136,7 +1136,7 @@ Section arc.
     iMod (bor_acc_cons with "LFT Hrc' Hα1") as "[Hrc' Hclose2]"=>//.
     iDestruct "Hrc'" as (rcvl) "[Hrc'↦ Hrc]".
     destruct rcvl as [|[[|rc|]|][|]]; try by iDestruct "Hrc" as ">[]".
-    rewrite heap_mapsto_vec_singleton. wp_read.
+    rewrite heap_pointsto_vec_singleton. wp_read.
     iAssert (shared_arc_own rc ty tid)%I with "[>Hrc]" as "Hrc".
     { iDestruct "Hrc" as "[Hrc|$]"=>//. by iApply arc_own_share. }
     iDestruct "Hrc" as (γi γs γw γsw ν t q') "[#(Hi & Hs & #Hc) [Htok1 Htok2]]". wp_let.
@@ -1148,7 +1148,7 @@ Section arc.
       iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); [done..|set_solver|].
       wp_op. iIntros "(#Hν & Hrc2 & H†)". iModIntro.
       iMod ("Hclose2" with "[Hrc'↦ Hrc0 Hrc1 H†] Hrc2") as "[Hb Hα1]".
-      { iIntros "!> Hrc2". iExists [_]. rewrite heap_mapsto_vec_singleton.
+      { iIntros "!> Hrc2". iExists [_]. rewrite heap_pointsto_vec_singleton.
         iFrame. iLeft. by iFrame. }
       iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
       iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); #(rc +ₗ 2) ◁ &uniq{α}ty;
@@ -1163,7 +1163,7 @@ Section arc.
       iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); [done..|set_solver|].
       wp_apply wp_new=>//; [set_solver+|lia|].
       iIntros (l) "(H† & Hlvl & Hml) (#Hν & Hown & H†') !>". rewrite -!lock Nat2Z.id.
-      wp_let. wp_op. rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
+      wp_let. wp_op. rewrite !heap_pointsto_vec_cons shift_loc_assoc shift_loc_0.
       iDestruct "Hlvl" as "(Hrc0 & Hrc1 & Hrc2)". wp_write. wp_op. wp_write.
       wp_op. wp_op. iDestruct "Hown" as (vl) "[H↦ Hown]".
       iDestruct (ty_size_eq with "Hown") as %Hsz.
@@ -1172,7 +1172,7 @@ Section arc.
       iIntros "[H↦ H↦']". wp_seq. wp_write.
       iMod ("Hclose2" $! ((l +ₗ 2) ↦∗: ty_own ty tid)%I
         with "[Hrc'↦ Hrc0 Hrc1 H†] [H↦ Hown]") as "[Hb Hα1]"; [|by auto with iFrame|].
-      { iIntros "!> H↦". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+      { iIntros "!> H↦". iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame.
         iLeft. iFrame. iDestruct "H†" as "[?|%]"=>//. }
       iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
       iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); (#l +ₗ #2) ◁ &uniq{α}ty;
@@ -1185,7 +1185,7 @@ Section arc.
       iApply type_jump; solve_typing.
     - iIntros "[Htok Hν]". wp_case. wp_apply wp_new=>//.
       iIntros (l) "/= (H† & Hl & Hm)". wp_let. wp_op.
-      rewrite heap_mapsto_vec_singleton. wp_write. wp_let.
+      rewrite heap_pointsto_vec_singleton. wp_write. wp_let.
       wp_bind (of_val clone).
       iApply (wp_wand with "[Hna]").
       { iApply (Hclone _ [] $! _ 1%Qp with "LFT HE Hna"); rewrite /llctx_interp /tctx_interp //. }
@@ -1196,7 +1196,7 @@ Section arc.
       iApply (type_call_iris _ [α ⊓ ν] (α ⊓ ν) [_] with
               "LFT HE Hna Hαν Hclone [Hl H†]"); [solve_typing| |].
       { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
-        iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+        iFrame. iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame.
         iApply ty_shr_mono; last done. iApply lft_intersect_incl_r. }
       iIntros ([[|cl|]|]) "Hna Hαν Hcl //". wp_rec.
       iDestruct "Hcl" as "[Hcl Hcl†]". iDestruct "Hcl" as (vl) "[Hcl↦ Hown]".
@@ -1205,7 +1205,7 @@ Section arc.
       wp_apply wp_new=>//. { lia. }
       iIntros (l') "(Hl'† & Hl' & Hm')". wp_let. wp_op.
       rewrite shift_loc_0. rewrite -!lock Nat2Z.id.
-      rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
+      rewrite !heap_pointsto_vec_cons shift_loc_assoc shift_loc_0.
       iDestruct "Hl'" as "(Hl' & Hl'1 & Hl'2)". wp_write. wp_op. wp_write. wp_op.
       wp_apply (wp_memcpy with "[$Hl'2 $Hcl↦]"); [done|..].
       { by rewrite repeat_length. } { by rewrite Hsz. }
@@ -1215,7 +1215,7 @@ Section arc.
       iIntros "_". wp_seq. wp_write.
       iMod ("Hclose2" $! ((l' +ₗ 2) ↦∗: ty_own ty tid)%I with
           "[Hrc'↦ Hl' Hl'1  Hl'†] [Hl'2 Hown]") as "[Hl' Hα1]".
-      { iIntros "!> H". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+      { iIntros "!> H". iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame.
         iLeft. iFrame. iDestruct "Hl'†" as "[?|%]"=>//. }
       { iExists _.  iFrame. }
       iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index d2d8fc0f1e68cea6a3ca410b8c77951a01fd778e..52971aaf3299543a5459b6286d7002a928b7e381 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -141,8 +141,8 @@ Section brandedvec.
     { iNext. iDestruct (ty_size_eq with "Hown'") as %->. done. }
     destruct vl' as [|v' vl']; first done.
     destruct vl' as [|]; last first. { simpl in *. lia. }
-    rewrite !heap_mapsto_vec_singleton.
-    iDestruct (heap_mapsto_agree with "Hmt1 Hmt2") as %->.
+    rewrite !heap_pointsto_vec_singleton.
+    iDestruct (heap_pointsto_agree with "Hmt1 Hmt2") as %->.
     iCombine "Hmt1" "Hmt2" as "Hmt".
     iApply "Hclose". done.
   Qed.
@@ -187,7 +187,7 @@ Section typing.
     wp_case.
     wp_alloc n as "Hm" "Hn" "Hdead".
     wp_let.
-    rewrite !heap_mapsto_vec_singleton.
+    rewrite !heap_pointsto_vec_singleton.
     wp_write.
     iAssert (∀ E : coPset, ⌜↑lftN ⊆ E⌝ →
       |={E}=> ∃ α, tctx_elt_interp tid ((LitV n : expr) ◁ box (brandvec α)) ∗ 1.[α])%I
@@ -198,7 +198,7 @@ Section typing.
       iExists α.
       rewrite !tctx_hasty_val.
       rewrite ownptr_own.
-      rewrite -heap_mapsto_vec_singleton.
+      rewrite -heap_pointsto_vec_singleton.
       iFrame "Htok".
       iExists n, (Vector.cons (LitV 0) Vector.nil).
       iSplitR; first done.
@@ -277,7 +277,7 @@ Section typing.
     iDestruct "Hv'" as (m) "#[Hghost Hmem]".
     iMod (lctx_lft_alive_tok β with "HE HL") as (qβ) "(Hβ & HL & Hclose)"; [solve_typing..|].
     iMod (frac_bor_acc with "LFT Hmem Hβ") as (qβ') "[>Hn'↦ Hcloseβ]"; first done.
-    rewrite !heap_mapsto_vec_singleton.
+    rewrite !heap_pointsto_vec_singleton.
     wp_read.
     iMod ("Hcloseβ" with "Hn'↦") as "Hβ".
     wp_op.
@@ -342,7 +342,7 @@ Section typing.
     iMod (lctx_lft_alive_tok β with "HE HL") as (qβ) "((Hβ1 & Hβ2 & Hβ3) & HL & Hclose)"; [solve_typing..|].
     iMod (frac_bor_acc with "LFT Hn Hβ1") as (qβn) "[>Hn↦ Hcloseβ1]"; first solve_ndisj.
     iMod (frac_bor_acc with "LFT Hm Hβ2") as (qβm) "[>Hm↦ Hcloseβ2]"; first solve_ndisj.
-    rewrite !heap_mapsto_vec_singleton.
+    rewrite !heap_pointsto_vec_singleton.
     wp_read.
     wp_op.
     wp_read.
@@ -390,7 +390,7 @@ Section typing.
     iMod (bor_acc with "LFT Hn Hβ") as "[H↦ Hclose']"; first solve_ndisj.
     iDestruct "H↦" as (vl) "[> H↦ Hn]".
     iDestruct "Hn" as (n) "[Hn > %]". simplify_eq.
-    rewrite !heap_mapsto_vec_singleton.
+    rewrite !heap_pointsto_vec_singleton.
     wp_read.
     wp_let.
     wp_op.
@@ -404,7 +404,7 @@ Section typing.
     iDestruct "Hlb" as "#Hlb".
     iMod ("Hclose'" with "[H↦ Hidx Hown]") as "[Hn Hβ]".
     { iExists (#(n+1)::nil).
-      rewrite heap_mapsto_vec_singleton.
+      rewrite heap_pointsto_vec_singleton.
       iFrame "∗".
       iIntros "!>".
       iExists (n + 1)%nat.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 03d565f084a94950e90161725fe087aa068bb9d6..4bcf5adf008d9faff39a804f020a3172df3644b5 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -64,7 +64,7 @@ Section cell.
       { iExists vl. by iFrame. }
       iModIntro. iSplitL "".
       { iNext. iExists vl. destruct vl; last done. iFrame "Hown".
-        by iApply heap_mapsto_vec_nil. }
+        by iApply heap_pointsto_vec_nil. }
       by iIntros "$ _". }
     (* Now we are in the non-0 case. *)
     iMod (na_bor_acc with "LFT Hshr Htok Htl") as "($ & Htl & Hclose)"; [solve_ndisj..|].
diff --git a/theories/typing/lib/fake_shared.v b/theories/typing/lib/fake_shared.v
index 4efaf32f616baa1dd44b4b1ddd8b7b1dac08dad5..a9aefbafe6528b34e2be23d9f8210d3450e41f74 100644
--- a/theories/typing/lib/fake_shared.v
+++ b/theories/typing/lib/fake_shared.v
@@ -23,7 +23,7 @@ Section fake_shared.
       iExists _. iFrame. iDestruct "H" as (vl) "[#Hf H]".
       iNext. destruct vl as [|[[|l'|]|][]]; try done. iExists l'. iSplit.
       { iApply frac_bor_iff; last done. iIntros "!>!> *".
-        rewrite heap_mapsto_vec_singleton. iSplit; auto. }
+        rewrite heap_pointsto_vec_singleton. iSplit; auto. }
       iDestruct "H" as "#H". iIntros "!> * % $".
       iApply step_fupd_intro. { set_solver. }
       simpl. iApply ty_shr_mono; last done.
@@ -55,7 +55,7 @@ Section fake_shared.
       iExists _. iFrame. iDestruct "H" as (vl) "[#Hf H]".
       iNext. destruct vl as [|[[|l'|]|][]]; try done. iExists l'. iSplit.
       { iApply frac_bor_iff; last done. iIntros "!>!> *".
-        rewrite heap_mapsto_vec_singleton. iSplit; auto. }
+        rewrite heap_pointsto_vec_singleton. iSplit; auto. }
       iDestruct "H" as "#H". iIntros "!> * % $".
       iApply step_fupd_intro. { set_solver. }
       simpl. iApply ty_shr_mono; last done.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index ffd35d9dfc188062c27098a86cdead49f8267570..7102dfbfc34901e798af801314673c517e828677 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -41,7 +41,7 @@ Section mutex.
     iIntros (ty E κ l tid q ?) "#LFT Hbor Htok".
     iMod (bor_acc_cons with "LFT Hbor Htok") as "[H Hclose]"; first done.
     iDestruct "H" as ([|[[| |n]|]vl]) "[H↦ [#hInv H]]"; try iDestruct "H" as ">[]".
-    rewrite heap_mapsto_vec_cons. iDestruct "H↦" as ">[Hl H↦]".
+    rewrite heap_pointsto_vec_cons. iDestruct "H↦" as ">[Hl H↦]".
     iDestruct "H" as "[>EQ Hown]". iDestruct "EQ" as %[b ->].
     (* We need to turn the ohne borrow into two, so we close it -- and then
        we open one of them again. *)
@@ -49,7 +49,7 @@ Section mutex.
           with "[] [Hl H↦ Hown]") as "[Hbor Htok]".
     { clear. iNext. iIntros "[Hl Hown] !>". iNext. iDestruct "Hl" as (b) "Hl".
       iDestruct "Hown" as (vl) "[H↦ Hown]". iExists (#(Z_of_bool b) :: vl).
-      rewrite heap_mapsto_vec_cons. iFrame "∗ hInv". iPureIntro. eauto. }
+      rewrite heap_pointsto_vec_cons. iFrame "∗ hInv". iPureIntro. eauto. }
     { iNext. iSplitL "Hl"; first by eauto.
       iExists vl. iFrame. }
     clear b vl. iMod (bor_sep with "LFT Hbor") as "[Hl Hbor]"; first done.
@@ -94,7 +94,7 @@ Section mutex.
       iExists _. iFrame "Hincl". iDestruct "Hshr" as (γ) "Hproto".
       iExists γ.
       iApply lock_proto_iff_proper; [|iFrame].
-      iApply bor_iff_proper. iApply heap_mapsto_pred_iff_proper.
+      iApply bor_iff_proper. iApply heap_pointsto_pred_iff_proper.
       iNext. iModIntro; iIntros; iSplit; iIntros; by iApply "Howni".
   Qed.
 
@@ -115,7 +115,7 @@ Section mutex.
     iIntros (???? l) "Hshr". iDestruct "Hshr" as (κ') "[Hincl Hshr]".
     iExists _. iFrame "Hincl". iDestruct "Hshr" as (γ) "Hproto".
     iExists γ. iApply lock_proto_iff_proper; [|iFrame].
-    iApply bor_iff_proper. iApply heap_mapsto_pred_iff_proper.
+    iApply bor_iff_proper. iApply heap_pointsto_pred_iff_proper.
     iNext. iModIntro; iIntros; iSplit; iIntros; by iApply send_change_tid.
   Qed.
 End mutex.
@@ -144,9 +144,9 @@ Section code.
     iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hm [Hx _]]".
     rewrite !tctx_hasty_val /=.
     iDestruct (ownptr_uninit_own with "Hm") as (lm vlm) "(% & Hm & Hm†)".
-    subst m. inv_vec vlm=>m vlm. simpl. iDestruct (heap_mapsto_vec_cons with "Hm") as "[Hm0 Hm]".
+    subst m. inv_vec vlm=>m vlm. simpl. iDestruct (heap_pointsto_vec_cons with "Hm") as "[Hm0 Hm]".
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
-    iDestruct (heap_mapsto_ty_own with "Hx") as (vl) "[>Hx Hxown]".
+    iDestruct (heap_pointsto_ty_own with "Hx") as (vl) "[>Hx Hxown]".
     (* All right, we are done preparing our context. Let's get going. *)
     wp_op. wp_apply (wp_memcpy with "[$Hm $Hx]"); [done|by rewrite vec_to_list_length..|].
     iIntros "[Hm Hx]". wp_seq. wp_op. rewrite shift_loc_0. wp_lam.
@@ -158,7 +158,7 @@ Section code.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val' // tctx_hasty_val' //.
       iFrame. iSplitL "Hx".
       - iExists _. iFrame. by rewrite uninit_own vec_to_list_length.
-      - iExists (#false :: vl). rewrite heap_mapsto_vec_cons.
+      - iExists (#false :: vl). rewrite heap_pointsto_vec_cons.
         iFrame "∗ HINV". eauto. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -182,9 +182,9 @@ Section code.
     iDestruct (ownptr_uninit_own with "Hx") as (lx vlx) "(% & Hx & Hx†)".
     subst x. simpl.
     destruct m as [[|lm|]|]; try done. iDestruct "Hm" as "[Hm Hm†]".
-    iDestruct (heap_mapsto_ty_own with "Hm") as (vlm) "[>Hm [#HINV Hvlm]]".
+    iDestruct (heap_pointsto_ty_own with "Hm") as (vlm) "[>Hm [#HINV Hvlm]]".
     inv_vec vlm=>m vlm. destruct m as [[|m|]|]; try by iDestruct "Hvlm" as ">[]".
-    simpl. iDestruct (heap_mapsto_vec_cons with "Hm") as "[Hm0 Hm]".
+    simpl. iDestruct (heap_pointsto_vec_cons with "Hm") as "[Hm0 Hm]".
     iDestruct "Hvlm" as "[_ Hvlm]".
     (* All right, we are done preparing our context. Let's get going. *)
     wp_op. wp_apply (wp_memcpy with "[$Hx $Hm]"); [done|by rewrite vec_to_list_length..|].
@@ -197,7 +197,7 @@ Section code.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val' // tctx_hasty_val' //.
       iFrame. iSplitR "Hm0 Hm".
       - iExists _. iFrame.
-      - iExists (_ :: _). rewrite heap_mapsto_vec_cons. iFrame.
+      - iExists (_ :: _). rewrite heap_pointsto_vec_cons. iFrame.
         rewrite uninit_own. rewrite /= vec_to_list_length. eauto. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -224,11 +224,11 @@ Section code.
     iMod (bor_acc_cons with "LFT Hm' Hα") as "[Hm' Hclose2]"; first done.
     wp_op. iDestruct "Hm'" as (vl) "[H↦ [#HINV Hm']]".
     destruct vl as [|[[|m'|]|] vl]; try done. simpl.
-    iDestruct (heap_mapsto_vec_cons with "H↦") as "[H↦1 H↦2]".
+    iDestruct (heap_pointsto_vec_cons with "H↦") as "[H↦1 H↦2]".
     iDestruct "Hm'" as "[% Hvl]".
     iMod ("Hclose2" $! ((lm' +ₗ 1) ↦∗: ty_own ty tid)%I with "[H↦1] [H↦2 Hvl]") as "[Hbor Hα]".
     { iIntros "!> Hlm' !>". iNext. clear vl. iDestruct "Hlm'" as (vl) "[H↦ Hlm']".
-      iExists (_ :: _). rewrite heap_mapsto_vec_cons. do 2 iFrame. iFrame "HINV". eauto. }
+      iExists (_ :: _). rewrite heap_pointsto_vec_cons. do 2 iFrame. iFrame "HINV". eauto. }
     { iExists vl. iFrame. }
     iMod ("Hclose1" with "Hα HL") as "HL".
     (* Switch back to typing mode. *)
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 9b2ac2524fef1b57e14ba6528531d6df5dcb4fe2..e9304df74d5e7c693e877e56fc87d1969d023aac 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -49,7 +49,7 @@ Section mguard.
     iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; [done|].
     destruct vl as [|[[|l'|]|][]];
       try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
-    setoid_rewrite heap_mapsto_vec_singleton.
+    setoid_rewrite heap_pointsto_vec_singleton.
     iMod (bor_exists with "LFT Hb") as (β) "Hb"; first done.
     iMod (bor_sep with "LFT Hb") as "[Hαβ H]"; first done.
     iMod (bor_sep with "LFT H") as "[_ H]"; first done.
@@ -99,10 +99,10 @@ Section mguard.
       + iDestruct "Hinv" as (γ) "Hproto".
         iExists γ. iApply lock_proto_lft_mono; first by iApply lft_incl_syn_sem.
         iApply lock_proto_iff_proper; [|iFrame].
-        iApply bor_iff_proper. iNext. iApply heap_mapsto_pred_iff_proper.
+        iApply bor_iff_proper. iNext. iApply heap_pointsto_pred_iff_proper.
         iModIntro; iIntros; iSplit; iIntros; by iApply "Ho".
       + iApply bor_iff; last done. iIntros "!>".
-        iApply heap_mapsto_pred_iff_proper.
+        iApply heap_pointsto_pred_iff_proper.
         iModIntro; iIntros; iSplit; iIntros; by iApply "Ho".
     - iIntros (κ tid l) "H". iDestruct "H" as (l') "H". iExists l'.
       iDestruct "H" as "[$ #H]". iIntros "!> * % Htok".
@@ -165,7 +165,7 @@ Section code.
     rewrite !tctx_hasty_val [[x]]lock /=.
     destruct m as [[|lm|]|]; try done. iDestruct "Hm" as (κ') "[#Hακ' #Hshr]".
     iDestruct (ownptr_uninit_own with "Hg") as (lg vlg) "(% & Hg & Hg†)".
-    subst g. inv_vec vlg=>g. rewrite heap_mapsto_vec_singleton.
+    subst g. inv_vec vlg=>g. rewrite heap_pointsto_vec_singleton.
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & HL & Hclose1)"; [solve_typing..|].
     iDestruct "Hshr" as (γ) "Hshr".
@@ -177,7 +177,7 @@ Section code.
         with "[] LFT HE Hna HL Hk"); last first.
     (* TODO: It would be nice to say [{#}] as the last spec pattern to clear the context in there. *)
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hg".
+      unlock. iFrame. iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame "Hg".
       iExists _. iFrame "#∗". iExists _. iFrame "#". }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -207,7 +207,7 @@ Section code.
       [solve_typing..|].
     destruct vl as [|[[|lm|]|] [|]]; simpl;
       try by iMod (bor_persistent with "LFT Hprot Hα") as "[>[] _]".
-    rewrite heap_mapsto_vec_singleton.
+    rewrite heap_pointsto_vec_singleton.
     iMod (bor_exists with "LFT Hprot") as (κ) "Hprot"; first done.
     iMod (bor_sep with "LFT Hprot") as "[Hβκ Hprot]"; first done.
     iMod (bor_sep with "LFT Hprot") as "[_ Hlm]"; first done.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 4eb224d632f5bece72bfc2773bdda776679b6656..eaf6cc423d8cf871b4713f4d9eec0ce69698b033 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -136,7 +136,7 @@ Section rc.
     iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
     destruct vl as [|[[|l'|]|][|]];
       try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
-    setoid_rewrite heap_mapsto_vec_singleton.
+    setoid_rewrite heap_pointsto_vec_singleton.
     iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
     iDestruct (monPred_in_intro with "Hb") as (V) "[#Hin Hb]".
     iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
@@ -222,7 +222,7 @@ Section rc.
     - iIntros (tid vl) "Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       iDestruct "Hvl" as "[(Hl1 & Hl2 & H† & Hc) | Hvl]".
       { iLeft. iFrame. iDestruct "Hsz" as %->.
-        iFrame. iApply (heap_mapsto_pred_wand with "Hc"). iApply "Hoincl". }
+        iFrame. iApply (heap_pointsto_pred_wand with "Hc"). iApply "Hoincl". }
       iDestruct "Hvl" as (γ ν q) "(#Hpersist & Htk & Hν)".
       iRight. iExists _, _, _. iFrame "#∗". by iApply rc_persist_type_incl.
     - iIntros "* #Hshr". iDestruct "Hshr" as (l') "[Hfrac Hshr]". iExists l'.
@@ -531,11 +531,11 @@ Section code.
     iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
     iDestruct (ownptr_uninit_own with "Hrcbox")
       as (lrcbox vlrcbox) "(% & Hrcbox↦ & Hrcbox†)". subst rcbox. inv_vec vlrcbox=>???.
-    iDestruct (heap_mapsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
-    iDestruct (heap_mapsto_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
+    iDestruct (heap_pointsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
+    iDestruct (heap_pointsto_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
     rewrite shift_loc_assoc.
     iDestruct (ownptr_uninit_own with "Hrc") as (lrc vlrc) "(% & Hrc↦ & Hrc†)". subst rc.
-    inv_vec vlrc=>?. rewrite heap_mapsto_vec_singleton.
+    inv_vec vlrc=>?. rewrite heap_pointsto_vec_singleton.
     (* All right, we are done preparing our context. Let's get going. *)
     wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write.
     wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
@@ -546,7 +546,7 @@ Section code.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
       iSplitL "Hx↦".
       { iExists _. rewrite uninit_own. auto. }
-      iNext. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame. iLeft.
+      iNext. iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame. iLeft.
       rewrite freeable_sz_full_S. iFrame. iExists _. iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -573,7 +573,7 @@ Section code.
     rewrite !tctx_hasty_val [[x]]lock.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
-    subst r. inv_vec vlr=>r. rewrite heap_mapsto_vec_singleton.
+    subst r. inv_vec vlr=>r. rewrite heap_pointsto_vec_singleton.
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
     wp_bind (!_)%E.
@@ -613,7 +613,7 @@ Section code.
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       unlock. iFrame "Hx". iFrame "Hr†". iExists [# #l'].
-      rewrite heap_mapsto_vec_singleton /=. simpl. eauto 10 with iFrame. }
+      rewrite heap_pointsto_vec_singleton /=. simpl. eauto 10 with iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
@@ -635,7 +635,7 @@ Section code.
     iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrcx [#Hrc' [Hx _]]]".
     rewrite !tctx_hasty_val [[rcx]]lock.
     iDestruct (ownptr_uninit_own with "Hx") as (lrc2 vlrc2) "(% & Hx & Hx†)".
-    subst x. inv_vec vlrc2=>?. rewrite heap_mapsto_vec_singleton.
+    subst x. inv_vec vlrc2=>?. rewrite heap_pointsto_vec_singleton.
     destruct rc' as [[|rc'|]|]; try done. simpl of_val.
     iDestruct "Hrc'" as (l') "[Hrc' #Hdelay]".
     (* All right, we are done preparing our context. Let's get going. *)
@@ -654,7 +654,7 @@ Section code.
     iApply (type_type _ _ _ [ rcx ◁ box (&shr{α}(rc ty)); #lrc2 ◁ box (&shr{α}ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite heap_mapsto_vec_singleton.
+      unlock. iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite heap_pointsto_vec_singleton.
       iFrame "Hx". by iApply ty_shr_mono. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -734,7 +734,7 @@ Section code.
         { unlock. rewrite 3!tctx_interp_cons tctx_interp_singleton. iFrame "Hr Hrc".
           rewrite 1!tctx_hasty_val tctx_hasty_val' //. iFrame "Hrcx".
           rewrite shift_loc_0 /=. iFrame. iExists [_; _].
-          rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+          rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
           auto with iFrame. }
         iApply (type_delete (Π[uninit 2;uninit ty.(ty_size)])); [solve_typing..|].
         iApply type_jump; solve_typing.
@@ -829,7 +829,7 @@ Section code.
         { unlock. rewrite 3!tctx_interp_cons tctx_interp_singleton. iFrame "Hr Hrc".
           rewrite 1!tctx_hasty_val tctx_hasty_val' //. iFrame "Hrcx".
           rewrite shift_loc_0 /=. iFrame. iExists [_; _].
-          rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+          rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
           auto with iFrame. }
         iApply (type_delete (Π[uninit 2;uninit ty.(ty_size)])); [solve_typing..|].
         iApply type_jump; solve_typing.
@@ -892,8 +892,8 @@ Section code.
     destruct rc' as [[|rc'|]|]; try done.
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & HL & Hclose1)"; [solve_typing..|].
     iMod (bor_acc_cons with "LFT Hrc' Hα") as "[Hrc' Hclose2]"; first solve_ndisj.
-    iDestruct (heap_mapsto_ty_own with "Hrc'") as (vl) "[>Hrc' Hrcown]".
-    inv_vec vl=>l. rewrite heap_mapsto_vec_singleton.
+    iDestruct (heap_pointsto_ty_own with "Hrc'") as (vl) "[>Hrc' Hrcown]".
+    inv_vec vl=>l. rewrite heap_pointsto_vec_singleton.
     wp_read. destruct l as [[|l|]|]; try done.
     wp_let. wp_op. rewrite shift_loc_0.
     wp_apply (rc_check_unique with "[$Hna Hrcown]"); first done.
@@ -906,7 +906,7 @@ Section code.
       + subst. wp_bind (#1 = #1)%E. iApply (wp_step_fupd with "Hrc"); [done..|].
         wp_op. iIntros "(Hl† & Hty & Hna)!>". wp_if.
         iMod ("Hclose2" with "[Hrc' Hl1 Hl2 Hl†] [Hty]") as "[Hty Hα]"; [|iNext; iExact "Hty"|].
-        { iIntros "!> Hty". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hrc'".
+        { iIntros "!> Hty". iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame "Hrc'".
           iLeft. by iFrame. }
         iMod ("Hclose1" with "Hα HL") as "HL".
         iApply (type_type _ _ _ [ r ◁ box (uninit 2); #l +ₗ #2 ◁ &uniq{α}ty;
@@ -919,7 +919,7 @@ Section code.
       + wp_op; case_bool_decide; first lia. wp_if. iMod ("Hrc" with "Hl1 Hl2") as "[Hna Hrc]".
         iMod ("Hclose2" with "[] [Hrc' Hrc]") as "[Hrc' Hα]".
         { iIntros "!> HX". iModIntro. iExact "HX". }
-        { iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame. auto. }
+        { iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame. auto. }
         iMod ("Hclose1" with "Hα HL") as "HL".
         iApply (type_type _ _ _ [ r ◁ box (uninit 2); rcx ◁ box (uninit 1)]
                 with "[] LFT HE Hna HL Hk [-]"); last first.
@@ -931,7 +931,7 @@ Section code.
       iMod ("Hproto" with "Hl1") as "[Hna Hrc]".
       iMod ("Hclose2" with "[] [Hrc' Hrc]") as "[Hrc' Hα]".
       { iIntros "!> HX". iModIntro. iExact "HX". }
-      { iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame. auto. }
+      { iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame. auto. }
       iMod ("Hclose1" with "Hα HL") as "HL".
       iApply (type_type _ _ _ [ r ◁ box (uninit 2); rcx ◁ box (uninit 1)]
               with "[] LFT HE Hna HL Hk [-]"); last first.
@@ -1025,8 +1025,8 @@ Section code.
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)";
       [solve_typing..|].
     iMod (bor_acc_cons with "LFT Hrc' Hα1") as "[Hrc' Hclose2]"; first solve_ndisj.
-    iDestruct (heap_mapsto_ty_own with "Hrc'") as (vl) "[>Hrc' Hrcown]".
-    inv_vec vl=>l. rewrite heap_mapsto_vec_singleton.
+    iDestruct (heap_pointsto_ty_own with "Hrc'") as (vl) "[>Hrc' Hrcown]".
+    inv_vec vl=>l. rewrite heap_pointsto_vec_singleton.
     wp_read. destruct l as [[|l|]|]; try done. wp_let. wp_op. rewrite shift_loc_0.
     wp_apply (rc_check_unique with "[$Hna Hrcown]"); first done.
     { (* Boy this is silly... *) iDestruct "Hrcown" as "[(?&?&?&?)|?]"; last by iRight.
@@ -1038,7 +1038,7 @@ Section code.
       + subst. wp_bind (#1 = #1)%E. iApply (wp_step_fupd with "Hrc"); [done..|].
         wp_op. iIntros "(Hl† & Hty & Hna)!>". wp_if.
         iMod ("Hclose2" with "[Hrc' Hl1 Hl2 Hl†] [Hty]") as "[Hty Hα1]"; [|iNext; iExact "Hty"|].
-        { iIntros "!> Hty". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hrc'".
+        { iIntros "!> Hty". iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame "Hrc'".
           iLeft. by iFrame. }
         iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
         iApply (type_type _ _ _ [ r ◁ box (uninit 1); #l +ₗ #2 ◁ &uniq{α}ty;
@@ -1053,7 +1053,7 @@ Section code.
         iApply (wp_step_fupd with "Hrc"); [done..|]. iApply wp_new; [set_solver+|lia|done|].
         rewrite -!lock Nat2Z.id.
         iNext. iIntros (lr) "/= ([H†|%] & H↦lr & Hm) [Hty Hproto] !>"; last lia.
-        rewrite 2!heap_mapsto_vec_cons. iDestruct "H↦lr" as "(Hlr1 & Hlr2 & Hlr3)".
+        rewrite 2!heap_pointsto_vec_cons. iDestruct "H↦lr" as "(Hlr1 & Hlr2 & Hlr3)".
         wp_let. wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write. wp_op. wp_op.
         iDestruct "Hty" as (vlr) "[H↦vlr Hty]". rewrite shift_loc_assoc.
         iDestruct (ty_size_eq with "Hty") as %Hsz.
@@ -1063,7 +1063,7 @@ Section code.
         iMod ("Hproto" with "[Hvlr]") as "Hna"; first by eauto.
         iMod ("Hclose2" $! ((lr +ₗ 2) ↦∗: ty_own ty tid)%I
               with "[Hrc' Hlr1 Hlr2 H†] [Hlr3 Hty]") as "[Hb Hα1]".
-        { iIntros "!> H !>". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+        { iIntros "!> H !>". iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame.
           iLeft. iFrame. }
         { iExists _. iFrame. }
         iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
@@ -1078,7 +1078,7 @@ Section code.
       iIntros (lr) "/= ([H†|%] & H↦lr & Hm)"; last lia.
       iDestruct "Hc" as "[[% ?]|[% [Hproto _]]]"; first lia.
       iMod ("Hproto" with "Hl1") as "[Hna Hty]". wp_let. wp_op.
-      rewrite heap_mapsto_vec_singleton. wp_write.
+      rewrite heap_pointsto_vec_singleton. wp_write.
       iAssert (∃ γ ν q, rc_persist tid ν γ l ty ∗ ⎡own γ (rc_tok q)⎤ ∗ q.[ν])%I
         with "[>Hty]" as (γ ν q') "(Hty & Htok & Hν)".
       { iDestruct "Hty" as "[(Hl1 & Hl2 & Hl† & Hl3)|Hty]"; last done.
@@ -1104,7 +1104,7 @@ Section code.
       iApply (type_call_iris _ [α ⊓ ν] (α ⊓ ν) [_]
               with "LFT HE Hna Hαν Hclone [H† H↦lr]"); [solve_typing| |].
       { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full_S.
-        iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+        iFrame. iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame.
         iApply ty_shr_mono; last done. iApply lft_intersect_incl_r. }
       iIntros ([[|cl|]|]) "Hna Hαν Hcl //". wp_rec.
       iDestruct "Hcl" as "[Hcl Hcl†]". iDestruct "Hcl" as (vl) "[Hcl↦ Hown]".
@@ -1113,7 +1113,7 @@ Section code.
       wp_apply wp_new=>//. { lia. }
       iIntros (l') "(Hl'† & Hl' & Hm')". wp_let. wp_op.
       rewrite shift_loc_0. rewrite -!lock Nat2Z.id.
-      rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
+      rewrite !heap_pointsto_vec_cons shift_loc_assoc shift_loc_0.
       iDestruct "Hl'" as "(Hl' & Hl'1 & Hl'2)". wp_write. wp_op. wp_write. wp_op.
       wp_apply (wp_memcpy with "[$Hl'2 $Hcl↦]");
         [by rewrite ?repeat_length ?Hsz //..|].
@@ -1123,7 +1123,7 @@ Section code.
       iIntros "_". wp_seq. wp_write.
       iMod ("Hclose2" $! ((l' +ₗ 2) ↦∗: ty_own ty tid)%I with
           "[Hrc' Hl' Hl'1  Hl'†] [Hl'2 Hown]") as "[Hl' Hα1]".
-      { iIntros "!> H". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+      { iIntros "!> H". iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame.
         iLeft. iFrame. iDestruct "Hl'†" as "[?|%]"=>//. }
       { iExists _.  iFrame. }
       iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 4bf178dcc8ce4cf91fac4411f76ba563656f8d30..35fbe7be394d1cbf1ac1c350a316459b07ef266e 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -32,7 +32,7 @@ Section weak.
     iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
     destruct vl as [|[[|l'|]|][|]];
       try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
-    setoid_rewrite heap_mapsto_vec_singleton.
+    setoid_rewrite heap_pointsto_vec_singleton.
     iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
     iDestruct (monPred_in_intro with "Hb") as (V) "[#Hin Hb]".
     iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
@@ -146,7 +146,7 @@ Section code.
     rewrite !tctx_hasty_val [[w]]lock.
     destruct w' as [[|lw|]|]; try done. iDestruct "Hw'" as (l') "[#Hlw #Hshr]".
     iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
-    subst r. inv_vec vlr=>r0 r1. rewrite !heap_mapsto_vec_cons.
+    subst r. inv_vec vlr=>r0 r1. rewrite !heap_pointsto_vec_cons.
     iDestruct "Hr" as "(Hr1 & Hr2 & _)".
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
@@ -188,7 +188,7 @@ Section code.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton tctx_hasty_val !tctx_hasty_val' //.
         unlock. iFrame "Hr† Hw". iSplitL "Hr1 Hr2".
         - iExists [_;_].
-          rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. auto with iFrame.
+          rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton. auto with iFrame.
         - iRight. auto with iFrame. }
       iApply (type_sum_assign (option (rc ty))); [solve_typing..|].
       iApply type_jump; solve_typing.
@@ -205,7 +205,7 @@ Section code.
           with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
         unlock. iFrame. iExists [_;_].
-        rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. auto with iFrame. }
+        rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton. auto with iFrame. }
       iApply (type_sum_unit (option (rc ty))); [solve_typing..|].
       iApply type_jump; solve_typing.
     - (* Failure : general case *)
@@ -221,7 +221,7 @@ Section code.
           with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
         unlock. iFrame. iExists [_;_].
-        rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. auto with iFrame. }
+        rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton. auto with iFrame. }
       iApply (type_sum_unit (option (rc ty))); [solve_typing..|].
       iApply type_jump; solve_typing.
   Qed.
@@ -248,7 +248,7 @@ Section code.
     rewrite !tctx_hasty_val [[x]]lock.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
-    subst r. inv_vec vlr=>r. rewrite heap_mapsto_vec_singleton.
+    subst r. inv_vec vlr=>r. rewrite heap_pointsto_vec_singleton.
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
     wp_bind (!_)%E.
@@ -283,7 +283,7 @@ Section code.
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       unlock. iFrame "Hx". iFrame "Hr†". iExists [# #l'].
-      rewrite heap_mapsto_vec_singleton /=. eauto 10 with iFrame. }
+      rewrite heap_pointsto_vec_singleton /=. eauto 10 with iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
@@ -311,7 +311,7 @@ Section code.
     rewrite !tctx_hasty_val [[x]]lock.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
-    subst r. inv_vec vlr=>r. rewrite heap_mapsto_vec_singleton.
+    subst r. inv_vec vlr=>r. rewrite heap_pointsto_vec_singleton.
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
     wp_bind (!_)%E.
@@ -355,7 +355,7 @@ Section code.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α}(weak ty)); #lr ◁ box (weak ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. iExists [# #l']. rewrite heap_mapsto_vec_singleton /=.
+      unlock. iFrame. iExists [# #l']. rewrite heap_pointsto_vec_singleton /=.
       auto 10 with iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -430,7 +430,7 @@ Section code.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
         unlock. iFrame. iDestruct "H" as (?) "(? & H↦ & ?)". iDestruct "H↦" as (?) "[? %]".
         rewrite /= freeable_sz_full_S. iFrame. iExists (_::_::_).
-        rewrite 2!heap_mapsto_vec_cons shift_loc_assoc. iFrame.
+        rewrite 2!heap_pointsto_vec_cons shift_loc_assoc. iFrame.
         iIntros "!> !%". simpl. congruence. }
       iApply type_delete; [try solve_typing..|].
       iApply type_jump; solve_typing.
@@ -461,10 +461,10 @@ Section code.
     iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hw [Hrcbox _]]". rewrite !tctx_hasty_val.
     iDestruct (ownptr_uninit_own with "Hrcbox") as (lrcbox vlrcbox)
        "(% & Hrcbox↦ & Hrcbox†)". subst rcbox. inv_vec vlrcbox=>??? /=.
-    iDestruct (heap_mapsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
-    iDestruct (heap_mapsto_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
+    iDestruct (heap_pointsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
+    iDestruct (heap_pointsto_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
     iDestruct (ownptr_uninit_own with "Hw") as (lw vlw) "(% & Hw↦ & Hw†)". subst w.
-    inv_vec vlw=>?. rewrite heap_mapsto_vec_singleton.
+    inv_vec vlw=>?. rewrite heap_pointsto_vec_singleton.
     (* All right, we are done preparing our context. Let's get going. *)
     wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write.
     iMod (lft_create with "LFT") as (ν) "[Hν #Hν†]"; first done.
@@ -474,7 +474,7 @@ Section code.
     iApply (type_type _ _ _ [ #lw ◁ box (weak ty)]
         with "[] LFT HE Hna HL Hk [> -]"); last first.
     { rewrite tctx_interp_singleton tctx_hasty_val' //=. iFrame.
-      iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+      iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame.
       iMod (own_alloc (● _ ⋅ ◯ _)) as (γ) "[??]"; last (iExists _, _; iFrame).
       { apply auth_both_valid_discrete. by split. }
       iExists ty. iFrame "Hν†". iSplitR; first by iApply type_incl_refl.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index ba589a064fa4c94f2a8bcb4f2e443d46148cdb8a..c3db62218ec057ad0fa7355de1fd8e0d878aca02 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -62,7 +62,7 @@ Section ref_functions.
     iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". { done. }
     iMod (na_bor_acc with "LFT Hinv Hδ Hna") as "(INV & Hna & Hcloseδ)"; [done..|].
     iMod (na_bor_acc with "LFT H◯inv Hα2 Hna") as "(H◯ & Hna & Hcloseα2)"; [solve_ndisj..|].
-    rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+    rewrite {1}heap_pointsto_vec_cons heap_pointsto_vec_singleton.
     iMod "H↦" as "[H↦1 H↦2]". wp_read. wp_let.
     iDestruct (refcell_inv_reading_inv with "INV Hâ—¯")
       as (q' n) "(H↦lrc & _ & [H● H◯] & H† & Hq' & Hshr')".
@@ -76,7 +76,7 @@ Section ref_functions.
         by apply Qp.add_le_mono_l, Qp.div_le. }
     wp_apply wp_new; [done..|]. iIntros (lr) "(?&Hlr&?)".
     iAssert (lx' ↦∗{qlx'} [ #lv; #lrc])%I  with "[H↦1 H↦2]" as "H↦".
-    { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
+    { rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton. iFrame. }
     wp_let. wp_apply (wp_memcpy with "[$Hlr $H↦]"); [done..|].
     iIntros "[Hlr H↦]". wp_seq. iMod ("Hcloseα2" with "[$H◯] Hna") as "[Hα1 Hna]".
     iMod ("Hcloseδ" with "[H↦lrc H● Hν1 Hshr' H†] Hna") as "[Hδ Hna]".
@@ -116,7 +116,7 @@ Section ref_functions.
     iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hx')".
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
     iMod (frac_bor_acc with "LFT Hfrac Hα") as (qlx') "[H↦ Hcloseα]". { done. }
-    rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+    rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
     iMod "H↦" as "[H↦1 H↦2]". wp_read. wp_let.
     iMod ("Hcloseα" with "[$H↦1 $H↦2]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
     iDestruct (lctx_lft_incl_incl α β with "HL HE") as %?; [solve_typing..|].
@@ -150,7 +150,7 @@ Section ref_functions.
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
     iDestruct "Hx" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hx"; simpl;
       try iDestruct "Hx" as "[_ >[]]".
-    rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+    rewrite {1}heap_pointsto_vec_cons heap_pointsto_vec_singleton.
     iDestruct "Hx" as "[[Hx↦1 Hx↦2] Hx]". wp_op. wp_read. wp_let.
     iDestruct "Hx" as (ν q γ β ty') "(_ & #Hαβ & #Hinv & Hν & H◯)".
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
@@ -187,7 +187,7 @@ Section ref_functions.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)] with "[] LFT HE Hna HL Hk");
       first last.
     { rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame. iExists [ #lv;#lrc].
-      rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton uninit_own. iFrame. auto. }
+      rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton uninit_own. iFrame. auto. }
     iApply type_delete; [solve_typing..|].
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_jump; solve_typing.
@@ -218,11 +218,11 @@ Section ref_functions.
     iDestruct "Href" as "[Href Href†]".
     iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href"; simpl;
       try iDestruct "Href" as "[_ >[]]".
-    rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+    rewrite {1}heap_pointsto_vec_cons heap_pointsto_vec_singleton.
     iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
     iDestruct "Href" as (ν qν γ β ty') "(#Hshr & #Hαβ & #Hinv & >Hν & Hγ)".
     wp_read. wp_let. wp_apply wp_new; try done.
-    iIntros (lx) "(H† & Hlx & ?)". rewrite heap_mapsto_vec_singleton.
+    iIntros (lx) "(H† & Hlx & ?)". rewrite heap_pointsto_vec_singleton.
     wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
     iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
     iMod (lctx_lft_alive_tok_noend ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
@@ -232,7 +232,7 @@ Section ref_functions.
     iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) [_; _]
        with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H†]"); [solve_typing|done| |].
     { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
-      iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. by iFrame. }
+      iFrame. iExists [_]. rewrite heap_pointsto_vec_singleton. by iFrame. }
     iIntros ([[|r|]|]) "Hna Hανϝ Hr //".
     iDestruct ("Hclose4" with "Hανϝ") as "[Hαν Hϝ]".
     iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
@@ -240,14 +240,14 @@ Section ref_functions.
     wp_rec. iDestruct "Hr" as "[Hr Hr†]".
     iDestruct "Hr" as ([|r'[]]) "[Hr #Hr']";
       try by iDestruct (ty_size_eq with "Hr'") as "%".
-    rewrite heap_mapsto_vec_singleton. wp_read. wp_let.
+    rewrite heap_pointsto_vec_singleton. wp_read. wp_let.
     wp_apply (wp_delete _ _ _ _ [_] with "[Hr Hr†]")=>//.
-    { rewrite heap_mapsto_vec_singleton freeable_sz_full. iFrame. } iIntros "_".
+    { rewrite heap_pointsto_vec_singleton freeable_sz_full. iFrame. } iIntros "_".
     wp_seq. wp_write.
     iApply (type_type _ [_] _ [ #lref ◁ box (ref α ty2) ]
        with "[] LFT HE Hna HL Hk"); first last.
     { rewrite tctx_interp_singleton tctx_hasty_val' //. simpl. iFrame.
-      iExists [_;_]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+      iExists [_;_]. rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
       iFrame. destruct r' as [[]|]=>//=. auto 10 with iFrame. }
     iApply type_jump; solve_typing.
   Qed.
@@ -297,11 +297,11 @@ Section ref_functions.
     iDestruct "Href" as "[Href Href†]".
     iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href"; simpl;
       try iDestruct "Href" as "[_ >[]]".
-    rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+    rewrite {1}heap_pointsto_vec_cons heap_pointsto_vec_singleton.
     iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
     iDestruct "Href" as (ν qν γ β ty') "(#Hshr & #Hαβ & #Hinv & >Hν & Hγ)".
     wp_read. wp_let. wp_apply wp_new; [done..|].
-    iIntros (lx) "(H† & Hlx & ?)". rewrite heap_mapsto_vec_singleton.
+    iIntros (lx) "(H† & Hlx & ?)". rewrite heap_pointsto_vec_singleton.
     wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
     iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
     iMod (lctx_lft_alive_tok_noend ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
@@ -311,7 +311,7 @@ Section ref_functions.
     iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) [_; _]
        with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H†]"); [solve_typing|done| |].
     { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
-      iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. by iFrame. }
+      iFrame. iExists [_]. rewrite heap_pointsto_vec_singleton. by iFrame. }
     iIntros ([[|r|]|]) "Hna Hανϝ Hr //".
     iDestruct ("Hclose4" with "Hανϝ") as "[Hαν Hϝ]".
     iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
@@ -320,10 +320,10 @@ Section ref_functions.
     iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 vl1' ->) "[#Hr1' H]".
     iDestruct "H" as (vl2 vl2' ->) "[#Hr2' ->]".
     destruct vl1 as [|[[|lr1|]|] []], vl2 as [|[[|lr2|]|] []]=>//=.
-    rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+    rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
     iDestruct "Hr" as "[Hr1 Hr2]". wp_read. wp_let. wp_op. wp_read. wp_let.
     wp_apply (wp_delete _ _ _ _ [_; _] with "[Hr1 Hr2 Hr†]")=>//.
-    { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
+    { rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton /= freeable_sz_full.
       iFrame. }
     iIntros "_".
     iMod (lft_incl_acc  with "Hαβ Hα") as (?) "[Hβ Hβclose]". { done. }
@@ -341,10 +341,10 @@ Section ref_functions.
         by apply Qp.add_le_mono_l, Qp.div_le. }
     wp_let. wp_read. wp_let. wp_op. wp_write.
     wp_apply (wp_delete _ _ _ _ [_; _] with "[Href↦1 Href↦2 Href†]")=>//.
-    { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
+    { rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton /= freeable_sz_full.
       iFrame. }
     iIntros "_". wp_seq. wp_apply wp_new; [done..|]. iIntros (lrefs) "(Hrefs† & Hrefs & ?)".
-    rewrite 3!heap_mapsto_vec_cons heap_mapsto_vec_singleton. wp_let.
+    rewrite 3!heap_pointsto_vec_cons heap_pointsto_vec_singleton. wp_let.
     iDestruct "Hrefs" as "(Hrefs1 & Hrefs2 & Hrefs3 & Hrefs4)".
     rewrite !shift_loc_assoc. wp_write. do 3 (wp_op; wp_write).
     iMod ("Hclosena" with "[H↦lrc H● Hν1 Hshr' H†] Hna") as "[Hβ Hna]".
@@ -356,7 +356,7 @@ Section ref_functions.
        with "[] LFT HE Hna HL Hk"); first last.
     { rewrite tctx_interp_singleton tctx_hasty_val' //= -freeable_sz_full.
       simpl. iFrame. iExists [_;_;_;_].
-      rewrite 3!heap_mapsto_vec_cons heap_mapsto_vec_singleton !shift_loc_assoc.
+      rewrite 3!heap_pointsto_vec_cons heap_pointsto_vec_singleton !shift_loc_assoc.
       iFrame. iExists [_;_], [_;_]. iSplit=>//=.
       iSplitL "Hν H◯"; [by auto 10 with iFrame|]. iExists [_;_], [].
       iSplitR=>//=. rewrite right_id. auto 20 with iFrame. }
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 5bc0bc919402befa28ef1a42584f378f850d4fd8..193d63151833d8b6c91a0656c9916d27944a6f8c 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -125,8 +125,8 @@ Section refcell.
             (l +ₗ 1) ↦∗: ty.(ty_own) tid) with "[] [-]")%I as "[H [Htok Htok']]".
     { iIntros "!> [Hn Hvl] !>". iDestruct "Hn" as (n') "Hn".
       iDestruct "Hvl" as (vl') "[H↦ Hvl]".
-      iExists (#n'::vl'). rewrite heap_mapsto_vec_cons. iFrame. }
-    { iNext. rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[Hn Hvl]".
+      iExists (#n'::vl'). rewrite heap_pointsto_vec_cons. iFrame. }
+    { iNext. rewrite heap_pointsto_vec_cons. iDestruct "H↦" as "[Hn Hvl]".
       iSplitL "Hn"; eauto with iFrame. }
     iMod (bor_sep with "LFT H") as "[Hn Hvl]". { done. }
     iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]". { done. }
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index e745680a76f267e7823ab909d98e3a1cfce33c99..f71cc56329bfd0a3d2ea377da3bece1d88a77aa0 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -28,7 +28,7 @@ Section refcell_functions.
     iDestruct "HT" as "[Hr Hx]".
     iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
     iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr↦ & Hr†)". subst r.
-    inv_vec vlr=>??. iDestruct (heap_mapsto_vec_cons with "Hr↦") as "[Hr↦0 Hr↦1]". wp_op.
+    inv_vec vlr=>??. iDestruct (heap_pointsto_vec_cons with "Hr↦") as "[Hr↦0 Hr↦1]". wp_op.
     rewrite shift_loc_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
     wp_apply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [by auto using vec_to_list_length..|].
     iIntros "[Hr↦1 Hx↦]". wp_seq.
@@ -37,7 +37,7 @@ Section refcell_functions.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=.
       iFrame. iSplitL "Hx↦".
       - iExists _. rewrite uninit_own. auto.
-      - simpl. iFrame. iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame=>//=. }
+      - simpl. iFrame. iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame=>//=. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
@@ -62,7 +62,7 @@ Section refcell_functions.
     iDestruct "HT" as "[Hr Hx]".
     iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & >Hx↦ & Hx & Hx†)". subst x.
     inv_vec vlx=>-[[|?|?]|????] vl; simpl; try iDestruct "Hx" as ">[]".
-    iDestruct (heap_mapsto_vec_cons with "Hx↦") as "[Hx↦0 Hx↦1]".
+    iDestruct (heap_pointsto_vec_cons with "Hx↦") as "[Hx↦0 Hx↦1]".
     iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr↦ & Hr†)". subst r.
     wp_op. wp_apply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [by auto using vec_to_list_length..|].
     iIntros "[Hr↦ Hx↦1]". wp_seq.
@@ -70,7 +70,7 @@ Section refcell_functions.
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iSplitR "Hr↦ Hx".
-      - iExists (_::_). rewrite heap_mapsto_vec_cons uninit_own. iFrame.
+      - iExists (_::_). rewrite heap_pointsto_vec_cons uninit_own. iFrame.
         rewrite /= vec_to_list_length. auto.
       - iExists vl. iFrame. }
     iApply type_delete; [solve_typing..|].
@@ -97,11 +97,11 @@ Section refcell_functions.
         (&uniq{α} ty).(ty_own) tid [ #(lx' +ₗ 1)])%I with "[> Hx']" as "[_ Hx']".
     { iApply bor_sep; [done..|]. iApply (bor_proper with "Hx'"). iSplit.
       - iIntros "[H1 H2]". iDestruct "H1" as (z) "?". iDestruct "H2" as (vl) "[??]".
-        iExists (_::_). rewrite heap_mapsto_vec_cons /=. iFrame=>//=.
+        iExists (_::_). rewrite heap_pointsto_vec_cons /=. iFrame=>//=.
       - iIntros "H".
         iDestruct "H" as ([|[[| |z]|]vl]) "[H↦ H]";
           simpl; try iDestruct "H" as "[]".
-        rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦1 H↦2]".
+        rewrite heap_pointsto_vec_cons. iDestruct "H↦" as "[H↦1 H↦2]".
         iSplitL "H↦1"; eauto. iExists _. iFrame. }
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
     iDestruct "Hx" as (vl) "[Hx↦ Hx]". rewrite uninit_own. wp_op.
@@ -168,7 +168,7 @@ Section refcell_functions.
       simpl. iApply type_jump; solve_typing.
     - wp_op. wp_write. wp_apply wp_new; [done..|].
       iIntros (lref) "(H† & Hlref & Hlm)". wp_let.
-      rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+      rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
       iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
       iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
                        ty_shr ty (β ⊓ ν) tid (lx +ₗ 1) ∗
@@ -215,7 +215,7 @@ Section refcell_functions.
               with "[] LFT HE Hna HL Hk"); first last.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
         rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
-        iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+        iExists [_; _]. rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
         iFrame. simpl. iExists _, _, _, _, _. iFrame "∗#". iApply ty_shr_mono; try by auto.
         iApply lft_intersect_mono; [done|]. iApply lft_incl_refl. }
       iApply (type_sum_memcpy (option $ ref α ty)); [solve_typing..|].
@@ -268,7 +268,7 @@ Section refcell_functions.
     iDestruct "INV" as (st) "(Hlx & Hownst & Hb)". wp_read. wp_let. wp_op; case_bool_decide; wp_if.
     - wp_write. wp_apply wp_new; [done..|].
       iIntros (lref) "(H† & Hlref & Hm)". wp_let.
-      rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+      rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
       iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
       destruct st as [[[[ν []] s] n]|]; try done.
       iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". { done. }
@@ -293,7 +293,7 @@ Section refcell_functions.
               with "[] LFT HE Hna HL Hk"); first last.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
         rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
-        iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+        iExists [_; _]. rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
         iFrame. simpl.
         iExists _, _, _, _, _. iFrame "#∗". iApply (bor_shorten with "[] [$Hb]").
         iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index af534737450548070e4051a098dd22edd6396ba9..dc3cc2e95bf2d322cfdbe6c41717da97595dd796 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -29,7 +29,7 @@ Section refmut_functions.
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose')";
       [solve_typing..|].
     iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". { done. }
-    rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+    rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
     iMod (lctx_lft_alive_tok_noend β with "HE HL") as (qβ) "(Hβ & HL & Hclose'')";
       [solve_typing..|].
     iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
@@ -82,7 +82,7 @@ Section refmut_functions.
     unshelve (iMod (bor_fracture _ (λ q', (q * q').[ν])%I with "LFT H") as "H"=>//); try apply _; try done.
     { split. - by rewrite Qp.mul_1_r. - apply _. }
     iDestruct (frac_bor_lft_incl _ _ q with "LFT H") as "#Hαν". iClear "H".
-    rewrite heap_mapsto_vec_cons. iMod (bor_sep with "LFT H↦") as "[H↦ _]". { done. }
+    rewrite heap_pointsto_vec_cons. iMod (bor_sep with "LFT H↦") as "[H↦ _]". { done. }
     iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". { done. }
     wp_bind (!#lx')%E. iMod (bor_unnest with "LFT Hb") as "Hb"; first done.
     wp_read. wp_let. iMod "Hb".
@@ -118,7 +118,7 @@ Section refmut_functions.
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
     iDestruct "Hx" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hx"; simpl;
       try iDestruct "Hx" as "[_ >[]]".
-    rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+    rewrite {1}heap_pointsto_vec_cons heap_pointsto_vec_singleton.
     iDestruct "Hx" as "[[Hx↦1 Hx↦2] Hx]". wp_op. wp_read. wp_let.
     iDestruct "Hx" as (ν q γ β ty') "(Hb & #Hαβ & #Hinv & Hν & H◯)".
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)";
@@ -158,7 +158,7 @@ Section refmut_functions.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)]
             with "[] LFT HE Hna HL Hk"); last first.
     { rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame. iExists [ #lv;#lrc].
-      rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton uninit_own. iFrame. auto. }
+      rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton uninit_own. iFrame. auto. }
     iApply type_delete; [solve_typing..|].
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_jump; solve_typing.
@@ -189,11 +189,11 @@ Section refmut_functions.
     iDestruct "Href" as "[Href Href†]".
     iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href"; simpl;
       try iDestruct "Href" as "[_ >[]]".
-    rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+    rewrite {1}heap_pointsto_vec_cons heap_pointsto_vec_singleton.
     iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
     iDestruct "Href" as (ν q γ β ty') "(Hbor & #Hαβ & #Hinv & >Hν & Hγ)".
     wp_read. wp_let. wp_apply wp_new; [done..|].
-    iIntros (lx) "(H† & Hlx & ?)". rewrite heap_mapsto_vec_singleton.
+    iIntros (lx) "(H† & Hlx & ?)". rewrite heap_pointsto_vec_singleton.
     wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
     iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
     iMod (lctx_lft_alive_tok_noend ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
@@ -203,7 +203,7 @@ Section refmut_functions.
     iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) [_; _]
             with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H† Hbor]"); [solve_typing|done| |].
     { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
-      iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. by iFrame. }
+      iFrame. iExists [_]. rewrite heap_pointsto_vec_singleton. by iFrame. }
     iIntros ([[|r|]|]) "Hna Hανϝ Hr //".
     iDestruct ("Hclose4" with "Hανϝ") as "[Hαν Hϝ]".
     iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
@@ -211,14 +211,14 @@ Section refmut_functions.
     wp_rec. iDestruct "Hr" as "[Hr Hr†]".
     iDestruct "Hr" as ([|r'[]]) "[Hr Hr']";
       try by iDestruct (ty_size_eq with "Hr'") as "%".
-    rewrite heap_mapsto_vec_singleton. wp_read. wp_let.
+    rewrite heap_pointsto_vec_singleton. wp_read. wp_let.
     wp_apply (wp_delete _ _ _ _ [_] with "[Hr Hr†]")=>//.
-    { rewrite heap_mapsto_vec_singleton freeable_sz_full. iFrame. } iIntros "_".
+    { rewrite heap_pointsto_vec_singleton freeable_sz_full. iFrame. } iIntros "_".
     wp_seq. wp_write.
     iApply (type_type _ [_] _ [ #lref ◁ box (refmut α ty2) ]
        with "[] LFT HE Hna HL Hk"); first last.
     { rewrite tctx_interp_singleton tctx_hasty_val' //. simpl. iFrame.
-      iExists [_;_]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+      iExists [_;_]. rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
       iFrame. destruct r' as [[]|]=>//=. auto 10 with iFrame. }
     iApply type_jump; solve_typing.
   Qed.
@@ -268,11 +268,11 @@ Section refmut_functions.
     iDestruct "Hrefmut" as "[Hrefmut Hrefmut†]".
     iDestruct "Hrefmut" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hrefmut"; simpl;
       try iDestruct "Hrefmut" as "[_ >[]]".
-    rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+    rewrite {1}heap_pointsto_vec_cons heap_pointsto_vec_singleton.
     iDestruct "Hrefmut" as "[[Hrefmut↦1 Hrefmut↦2] Hrefmut]".
     iDestruct "Hrefmut" as (ν qν γ β ty') "(Hbor & #Hαβ & #Hinv & >Hν & Hγ)".
     wp_read. wp_let. wp_apply wp_new; [done..|].
-    iIntros (lx) "(H† & Hlx & ?)". rewrite heap_mapsto_vec_singleton.
+    iIntros (lx) "(H† & Hlx & ?)". rewrite heap_pointsto_vec_singleton.
     wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
     iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
     iMod (lctx_lft_alive_tok_noend ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
@@ -282,7 +282,7 @@ Section refmut_functions.
     iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) [_; _]
        with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H† Hbor]"); [solve_typing|done| |].
     { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
-      iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. by iFrame. }
+      iFrame. iExists [_]. rewrite heap_pointsto_vec_singleton. by iFrame. }
     iIntros ([[|r|]|]) "Hna Hανϝ Hr //".
     iDestruct ("Hclose4" with "Hανϝ") as "[Hαν Hϝ]".
     iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
@@ -291,10 +291,10 @@ Section refmut_functions.
     iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 vl1' ->) "[Hr1' H]".
     iDestruct "H" as (vl2 vl2' ->) "[Hr2' ->]".
     destruct vl1 as [|[[|lr1|]|] []], vl2 as [|[[|lr2|]|] []]=>//=.
-    rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+    rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
     iDestruct "Hr" as "[Hr1 Hr2]". wp_read. wp_let. wp_op. wp_read. wp_let.
     wp_apply (wp_delete _ _ _ _ [_; _] with "[Hr1 Hr2 Hr†]")=>//.
-    { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
+    { rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton /= freeable_sz_full.
       iFrame. }
     iIntros "_".
     iMod (lft_incl_acc  with "Hαβ Hα") as (?) "[Hβ Hβclose]". { done. }
@@ -315,10 +315,10 @@ Section refmut_functions.
         by apply Qp.add_le_mono_l, Qp.div_le. }
     wp_let. wp_read. wp_let. wp_op. wp_write.
     wp_apply (wp_delete _ _ _ _ [_; _] with "[Hrefmut↦1 Hrefmut↦2 Hrefmut†]")=>//.
-    { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
+    { rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton /= freeable_sz_full.
       iFrame. }
     iIntros "_". wp_seq. wp_apply wp_new; [done..|]. iIntros (lrefmuts) "(Hrefmuts† & Hrefmuts & ?)".
-    rewrite 3!heap_mapsto_vec_cons heap_mapsto_vec_singleton. wp_let.
+    rewrite 3!heap_pointsto_vec_cons heap_pointsto_vec_singleton. wp_let.
     iDestruct "Hrefmuts" as "(Hrefmuts1 & Hrefmuts2 & Hrefmuts3 & Hrefmuts4)".
     rewrite !shift_loc_assoc. wp_write. do 3 (wp_op; wp_write).
     iMod ("Hclosena" with "[Hlrc H● Hν1 H†] Hna") as "[Hβ Hna]".
@@ -331,7 +331,7 @@ Section refmut_functions.
        with "[] LFT HE Hna HL Hk"); first last.
     { rewrite tctx_interp_singleton tctx_hasty_val' //= -freeable_sz_full.
       simpl. iFrame. iExists [_;_;_;_].
-      rewrite 3!heap_mapsto_vec_cons heap_mapsto_vec_singleton !shift_loc_assoc.
+      rewrite 3!heap_pointsto_vec_cons heap_pointsto_vec_singleton !shift_loc_assoc.
       iFrame. iExists [_;_], [_;_]. iSplit=>//=.
       iSplitL "Hν Hγ Hr1'"; [by auto 10 with iFrame|]. iExists [_;_], [].
       iSplitR=>//=. rewrite right_id. auto 20 with iFrame. }
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index c05cf674668a5b4de71763b9ba7881a039978e34..4d77b0af3367afb023389668c2d84479cba1f2c5 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -405,8 +405,8 @@ Section rwlock.
             (l +ₗ 1) ↦∗: ty.(ty_own) tid) with "[] [-]")%I as "[H Htok]".
     { iIntros "!> [Hn Hvl] !>". iDestruct "Hn" as (n') "[Hn >%]".
       iDestruct "Hvl" as (vl') "[H↦ Hvl]".
-      iExists (#n'::vl'). rewrite heap_mapsto_vec_cons. iFrame "∗% hInv". }
-    { iNext. rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[Hn Hvl]".
+      iExists (#n'::vl'). rewrite heap_pointsto_vec_cons. iFrame "∗% hInv". }
+    { iNext. rewrite heap_pointsto_vec_cons. iDestruct "H↦" as "[Hn Hvl]".
       iSplitL "Hn"; [eauto|iExists _; iFrame]. }
     iMod (bor_sep with "LFT H") as "[Hn Hvl]". { done. }
     iMod (rwlock_proto_create with "LFT Htok hInv Hvl Hn") as "[$ Hproto]". { done. }
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 39d39a629e732c97a63769087102f6c2b86a7990..6a816a428d96bba8a38d39f7b90eec91319e90eb 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -45,7 +45,7 @@ Section rwlock_functions.
     destruct r as [[|lr|]|]; try done. iDestruct "Hr" as "[Hr Hr†]".
     iDestruct "Hr" as (vl') "Hr". rewrite uninit_own.
     iDestruct "Hr" as "[Hr↦ >SZ]". destruct vl' as [|]; iDestruct "SZ" as %[=].
-    rewrite heap_mapsto_vec_cons. iDestruct "Hr↦" as "[Hr↦0 Hr↦1]". wp_op.
+    rewrite heap_pointsto_vec_cons. iDestruct "Hr↦" as "[Hr↦0 Hr↦1]". wp_op.
     rewrite shift_loc_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
     wp_apply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [done||lia..|].
     iIntros "[Hr↦1 Hx↦]". wp_seq.
@@ -55,7 +55,7 @@ Section rwlock_functions.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
       iSplitL "Hx↦".
       - iExists _. rewrite uninit_own. auto.
-      - iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. simpl. iFrame. auto. }
+      - iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame. simpl. iFrame. auto. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
@@ -80,7 +80,7 @@ Section rwlock_functions.
     iDestruct "Hx" as "[Hx Hx†]".
     iDestruct "Hx" as ([|[[]|]vl]) "[Hx↦ [HI Hx]]"; try iDestruct "Hx" as ">[]".
     destruct r as [[|lr|]|]; try done. iDestruct "Hr" as "[Hr Hr†]".
-    iDestruct "Hr" as (vl') "Hr". rewrite uninit_own heap_mapsto_vec_cons.
+    iDestruct "Hr" as (vl') "Hr". rewrite uninit_own heap_pointsto_vec_cons.
     iDestruct "Hr" as "[Hr↦ >%]". iDestruct "Hx↦" as "[Hx↦0 Hx↦1]". wp_op.
     iDestruct "Hx" as "[% Hx]". iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
     wp_apply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [done||lia..|].
@@ -89,7 +89,7 @@ Section rwlock_functions.
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iSplitR "Hr↦ Hx".
-      - iExists (_::_). rewrite heap_mapsto_vec_cons uninit_own -Hsz. iFrame. auto.
+      - iExists (_::_). rewrite heap_pointsto_vec_cons uninit_own -Hsz. iFrame. auto.
       - iExists vl. iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -115,9 +115,9 @@ Section rwlock_functions.
     { iApply bor_sep; [done..|]. iApply (bor_proper with "Hx'"). iSplit.
       - iIntros "[H1 H2]". iDestruct "H1" as "[? H1]".
         iDestruct "H1" as (z) "[??]". iDestruct "H2" as (vl) "[??]".
-        iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. iFrame.
+        iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame. iFrame.
       - iIntros "H". iDestruct "H" as ([|[[| |z]|]vl]) "[H↦ [HI H]]"; try done.
-        rewrite heap_mapsto_vec_cons. iFrame "HI".
+        rewrite heap_pointsto_vec_cons. iFrame "HI".
         iDestruct "H" as "[H1 H2]". iDestruct "H↦" as "[H↦1 H↦2]".
         iSplitL "H1 H↦1"; eauto. iExists _. iFrame. }
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index df763433722b22cb0f181117384cac54dbe5ac5f..98923018663f3ff393c05ee3746f1698bf440ef2 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -32,7 +32,7 @@ Section rwlockreadguard_functions.
     iDestruct "Hx'" as (l') "#[Hfrac Hshr]".
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
     iMod (frac_bor_acc with "LFT Hfrac Hα") as (qlx') "[H↦ Hcloseα]". { done. }
-    rewrite heap_mapsto_vec_singleton. wp_read. wp_op. wp_let.
+    rewrite heap_pointsto_vec_singleton. wp_read. wp_op. wp_let.
     iMod ("Hcloseα" with "[$H↦]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
     iDestruct (lctx_lft_incl_incl α β with "HL HE") as %?; [solve_typing..|].
     iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rwlockreadguard β ty));
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index ddf79195f615b72d2874e11991e0f504bf187728..8c71fb6c7a845903884b690111c6f3ddef286797 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -33,7 +33,7 @@ Section rwlockwriteguard_functions.
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose)";
       [solve_typing..|].
     iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". { done. }
-    rewrite heap_mapsto_vec_singleton.
+    rewrite heap_pointsto_vec_singleton.
     iMod (lctx_lft_alive_tok_noend β with "HE HL") as (qβ) "(Hβ & HL & Hclose')";
       [solve_typing..|].
     iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
@@ -79,7 +79,7 @@ Section rwlockwriteguard_functions.
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
     destruct vl as [|[[|l|]|][]];
       try by iMod (bor_persistent with "LFT H Hα") as "[>[] _]".
-    rewrite heap_mapsto_vec_singleton.
+    rewrite heap_pointsto_vec_singleton.
     iMod (bor_exists with "LFT H") as (γ) "H". { done. }
     iMod (bor_exists with "LFT H") as (δ) "H". { done. }
     iMod (bor_exists with "LFT H") as (tid_shr) "H". { done. }
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index c36ab18f4951e4dafd2924db2f3deba8ab7c5665..906d5a1818c3b4ba33a0f6cda193581e8ea4ee37 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -35,7 +35,7 @@ Section code.
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose1)"; [solve_typing..|].
     iMod (lctx_lft_alive_tok_noend ϝ with "HE HL") as (qϝ) "(Hϝ & HL & Hclose2)"; [solve_typing..|].
     iMod (bor_acc with "LFT Hx' Hα") as "[Hx' Hclose3]"; first done.
-    iDestruct (heap_mapsto_ty_own with "Hx'") as (x'vl) "[>Hx'↦ Hx'vl]".
+    iDestruct (heap_pointsto_ty_own with "Hx'") as (x'vl) "[>Hx'↦ Hx'vl]".
     wp_apply (wp_memcpy with "[$Htl $Hx'↦]"); [by auto using vec_to_list_length..|].
     iIntros "[Htl Hx'↦]". wp_seq.
     (* Call the function. *)
diff --git a/theories/typing/own.v b/theories/typing/own.v
index f17961728d3a730f4d48d892bbebde83611b8274..30dc609d51b88db2f48fba3f1a134a6badeadc79 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -70,7 +70,7 @@ Section own.
     iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]"; first solve_ndisj.
     destruct vl as [|[[|l'|]|][]];
       try (iMod (bor_persistent with "LFT Hb2 Htok") as "[>[]_]"; solve_ndisj).
-    iFrame. iExists l'. rewrite heap_mapsto_vec_singleton.
+    iFrame. iExists l'. rewrite heap_pointsto_vec_singleton.
     rewrite bi.later_sep.
     iMod (bor_sep with "LFT Hb2") as "[Hb2 _]"; first solve_ndisj.
     iMod (bor_fracture (l ↦{1} #l')%I with "LFT Hb1") as "$"; first solve_ndisj.
@@ -97,7 +97,7 @@ Section own.
     iIntros "#Heq (#Hsz & #Ho & #Hs)". iSplit; first done. iSplit; iModIntro.
     - iIntros (?[|[[| |]|][]]) "H"; try done. simpl.
       iDestruct "H" as "[Hmt H†]". iNext. iDestruct ("Hsz") as %<-.
-      iDestruct "Heq" as %->. iFrame. iApply (heap_mapsto_pred_wand with "Hmt").
+      iDestruct "Heq" as %->. iFrame. iApply (heap_pointsto_pred_wand with "Hmt").
       iApply "Ho".
     - iIntros (???) "H". iDestruct "H" as (l') "[Hfb #Hvs]".
       iExists l'. iFrame. iIntros "!>". iIntros (F' q) "% Htok".
@@ -133,7 +133,7 @@ Section own.
     Send ty → Send (own_ptr n ty).
   Proof.
     iIntros (Hsend tid1 tid2 [|[[| |]|][]]) "H"; try done.
-    iDestruct "H" as "[Hm $]". iNext. iApply (heap_mapsto_pred_wand with "Hm").
+    iDestruct "H" as "[Hm $]". iNext. iApply (heap_pointsto_pred_wand with "Hm").
     iIntros (vl) "?". by iApply Hsend.
   Qed.
 
@@ -194,7 +194,7 @@ Section util.
   Proof.
     iSplit.
     - iIntros "Hown". destruct v as [[|l|]|]; try done.
-      iExists l. iDestruct "Hown" as "[Hown $]". rewrite heap_mapsto_ty_own.
+      iExists l. iDestruct "Hown" as "[Hown $]". rewrite heap_pointsto_ty_own.
       iDestruct "Hown" as (vl) "[??]". eauto with iFrame.
     - iIntros "Hown". iDestruct "Hown" as (l vl) "(% & ? & ? & ?)". subst v.
       iFrame. iExists _. iFrame.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 976583fadb7ff1e7cc87efc043798bcf49ce0459..696d302c813f53e3228cf2b90832a4f7514fa8c2 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -25,7 +25,7 @@ Section product.
     split. { by apply _. } iIntros (????????) "_ _ Htok $".
     iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first solve_ndisj.
     iExists 1%Qp. iModIntro. iSplitR.
-    { iExists []. iSplitL; last by auto. rewrite heap_mapsto_vec_nil. auto. }
+    { iExists []. iSplitL; last by auto. rewrite heap_pointsto_vec_nil. auto. }
     iIntros "Htok2 _". iApply "Htok". done.
   Qed.
 
@@ -42,12 +42,12 @@ Section product.
   Proof.
     iSplit; iIntros "H".
     - iDestruct "H" as (vl) "[H↦ H]". iDestruct "H" as (vl1 vl2) "(% & H1 & H2)".
-      subst. rewrite heap_mapsto_vec_app. iDestruct "H↦" as "[H↦1 H↦2]".
+      subst. rewrite heap_pointsto_vec_app. iDestruct "H↦" as "[H↦1 H↦2]".
       iDestruct (ty_size_eq with "H1") as %->.
       iSplitL "H1 H↦1"; iExists _; iFrame.
     - iDestruct "H" as "[H1 H2]". iDestruct "H1" as (vl1) "[H↦1 H1]".
       iDestruct "H2" as (vl2) "[H↦2 H2]". iExists (vl1 ++ vl2).
-      rewrite heap_mapsto_vec_app. iDestruct (ty_size_eq with "H1") as %->.
+      rewrite heap_pointsto_vec_app. iDestruct (ty_size_eq with "H1") as %->.
       iFrame. iExists _, _. by iFrame.
   Qed.
 
@@ -134,8 +134,8 @@ Section product.
       iDestruct "H1" as (vl1') "[H↦1 H1]". iDestruct "H2" as (vl2') "[H↦2 H2]".
       iDestruct (ty_size_eq with "H1") as "#>%".
       iDestruct (ty_size_eq with "H2") as "#>%".
-      iDestruct (heap_mapsto_vec_combine with "H↦1 H↦1f") as "H↦1"; [congruence|].
-      iDestruct (heap_mapsto_vec_combine with "H↦2 H↦2f") as "H↦2"; [congruence|].
+      iDestruct (heap_pointsto_vec_combine with "H↦1 H↦1f") as "H↦1"; [congruence|].
+      iDestruct (heap_pointsto_vec_combine with "H↦2 H↦2f") as "H↦2"; [congruence|].
       iMod ("Hclose2" with "Htl [H2 H↦2]") as "[Htl $]".
       { by iExists _; iFrame. }
       iMod ("Hclose1" with "Htl [H1 H↦1]") as "[$$]".
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index d016750175831999cf41a5658a7eb3cdfe1d1fbf..7242ba715ab6b97e6fbcc3b30c7fae440ee8321d 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -92,7 +92,7 @@ Section product_split.
     iDestruct "H" as ([[]|]) "[#Hp H]"; try done.
     iDestruct "H" as "[H >H†]". iDestruct "H" as (vl) "[>H↦ H]".
     iDestruct "H" as (vl1 vl2) "(>% & H1 & H2)". subst.
-    rewrite heap_mapsto_vec_app -freeable_sz_split.
+    rewrite heap_pointsto_vec_app -freeable_sz_split.
     iDestruct "H†" as "[H†1 H†2]". iDestruct "H↦" as "[H↦1 H↦2]".
     iDestruct (ty_size_eq with "H1") as "#>EQ".
     iDestruct "EQ" as %->. iSplitL "H↦1 H†1 H1".
@@ -113,7 +113,7 @@ Section product_split.
     rewrite Hρ1. iDestruct "Hp2" as %[=<-]. iDestruct "H2" as "[H↦2 H†2]".
     iExists #_. iSplitR; first done. rewrite /= -freeable_sz_split Nat2Z.id. iFrame.
     iDestruct "H↦1" as (vl1) "[H↦1 H1]". iDestruct "H↦2" as (vl2) "[H↦2 H2]".
-    iExists (vl1 ++ vl2). rewrite heap_mapsto_vec_app. iFrame.
+    iExists (vl1 ++ vl2). rewrite heap_pointsto_vec_app. iFrame.
     iDestruct (ty_size_eq with "H1") as "#>EQ". iDestruct "EQ" as %->.
     rewrite {3}/ty_own /=. auto 10 with iFrame.
   Qed.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 9eab149ff066e1f95f16baa25bcfd5255c2d6641..d5c811cfb8eb402d17b0372e49a2052b44135e15 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -83,7 +83,7 @@ Section typing.
   Proof. rewrite typed_write_eq. apply _. Qed.
 
   (* Technically speaking, we could remvoe the vl quantifiaction here and use
-     mapsto_pred instead (i.e., l ↦∗: ty.(ty_own) tid). However, that would
+     pointsto_pred instead (i.e., l ↦∗: ty.(ty_own) tid). However, that would
      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. *)
@@ -256,8 +256,8 @@ Section typing_rules.
     iMod (Hwrt with "[] LFT HE HL Hown1") as (l vl) "([% %] & Hl & Hclose)"; first done.
     subst v1. iDestruct (ty_size_eq with "Hown2") as "#Hsz". iDestruct "Hsz" as %Hsz.
     rewrite <-Hsz in *. destruct vl as [|v[|]]; try done.
-    rewrite heap_mapsto_vec_singleton. iApply wp_fupd. wp_write.
-    rewrite -heap_mapsto_vec_singleton.
+    rewrite heap_pointsto_vec_singleton. iApply wp_fupd. wp_write.
+    rewrite -heap_pointsto_vec_singleton.
     iMod ("Hclose" with "[Hl Hown2]") as "(HL & Hown)".
     { iExists _. iFrame. }
     iDestruct ("HLclose" with "HL") as "$".
@@ -285,7 +285,7 @@ Section typing_rules.
         (l vl q [= ->]) "(Hl & Hown & Hclose)"; first done.
     iDestruct (ty_size_eq with "Hown") as "#>%". rewrite ->Hsz in *.
     destruct vl as [|v [|]]; try done.
-    rewrite heap_mapsto_vec_singleton. iApply wp_fupd. wp_read.
+    rewrite heap_pointsto_vec_singleton. iApply wp_fupd. wp_read.
     iMod ("Hclose" with "Hl") as "($ & HL & Hown2)".
     iDestruct ("HLclose" with "HL") as "$".
     rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 5f05f2d51e4a472b6a3663fdf86485ac1db05851..10ed7a06aa2c70b1fb1f0c973d0733449c85d09d 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -37,9 +37,9 @@ Section sum.
   Proof.
     iSplit; iIntros "H".
     - iDestruct "H" as (vl) "[Hmt Hown]". iDestruct "Hown" as (i vl' vl'') "(% & % & Hown)".
-      subst. iExists i. iDestruct (heap_mapsto_vec_cons with "Hmt") as "[$ Hmt]".
+      subst. iExists i. iDestruct (heap_pointsto_vec_cons with "Hmt") as "[$ Hmt]".
       iDestruct (ty_size_eq with "Hown") as "#EQ". iDestruct "EQ" as %Hvl'.
-      iDestruct (heap_mapsto_vec_app with "Hmt") as "[Hmt Htail]". iSplitL "Htail".
+      iDestruct (heap_pointsto_vec_app with "Hmt") as "[Hmt Htail]". iSplitL "Htail".
       + iExists vl''. rewrite (shift_loc_assoc_nat _ 1) Hvl'. iFrame. iPureIntro.
         rewrite -Hvl'. simpl in *. rewrite -app_length. congruence.
       + iExists vl'. by iFrame.
@@ -47,7 +47,7 @@ Section sum.
       iDestruct "Hown" as (vl') "[Hmt2 Hown]". iDestruct "Htail" as (vl'') "[Hmt3 %]".
       iDestruct (ty_size_eq with "Hown") as "#EQ". iDestruct "EQ" as %Hvl'.
       iExists (#i::vl'++vl'').
-      rewrite heap_mapsto_vec_cons heap_mapsto_vec_app (shift_loc_assoc_nat _ 1) Hvl'.
+      rewrite heap_pointsto_vec_cons heap_pointsto_vec_app (shift_loc_assoc_nat _ 1) Hvl'.
       iFrame. iExists i, vl', vl''. iSplit; first done. iFrame. iPureIntro.
       simpl. f_equal. by rewrite app_length Hvl'.
   Qed.
@@ -201,14 +201,14 @@ Section sum.
         - apply shr_locsE_subseteq. lia.
         - set_solver+. }
       destruct (Qp.lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
-      rewrite -(heap_mapsto_pred_combine _ q' q'02); last (by intros; iApply ty_size_eq).
+      rewrite -(heap_pointsto_pred_combine _ q' q'02); last (by intros; iApply ty_size_eq).
       rewrite (fractional (Φ := λ q, _ ↦{q} _ ∗ _ ↦∗{q}: _)%I).
       iDestruct "HownC" as "[HownC1 HownC2]". iDestruct "Hown" as "[Hown1 Hown2]".
       iExists q'. iModIntro. iSplitL "Hown1 HownC1".
       + iNext. iExists i. iFrame.
       + iIntros "Htl H". iDestruct "H" as (i') "[>Hown1 HownC1]".
         iDestruct ("Htlclose" with "Htl") as "Htl".
-        iDestruct (heap_mapsto_agree with "[Hown1] [Hown2]") as "#Heq".
+        iDestruct (heap_pointsto_agree with "[Hown1] [Hown2]") as "#Heq".
         { iDestruct "Hown1" as "[$ _]". } { iDestruct "Hown2" as "[$ _]". }
         iDestruct "Heq" as %[= ->%Nat2Z.inj].
         iMod ("Hclose'" with "Htl [$HownC1 $HownC2]") as "[$ ?]".
diff --git a/theories/typing/type.v b/theories/typing/type.v
index ae9b7185a52c0411c748f53e9bb8c5687e2386ee..e40f037bf38a1bf9429947f85de282be1281436a 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -504,7 +504,7 @@ Section type.
     { iNext. iDestruct (st_size_eq with "Hown") as %->.
       iDestruct (st_size_eq with "Hown'") as %->. done. }
     iApply "Hclose".
-    by iDestruct (heap_mapsto_vec_combine with "Hmt2 Hmt1") as "[$$]".
+    by iDestruct (heap_pointsto_vec_combine with "Hmt2 Hmt1") as "[$$]".
   Qed.
 
   (** Send and Sync types *)
@@ -751,7 +751,7 @@ End subtyping.
 Section type_util.
   Context `{!typeG Σ}.
 
-  Lemma heap_mapsto_ty_own l ty tid :
+  Lemma heap_pointsto_ty_own l ty tid :
     l ↦∗: ty_own ty tid ⊣⊢ ∃ (vl : vec val ty.(ty_size)), l ↦∗ vl ∗ ty_own ty tid vl.
   Proof.
     iSplit.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 55098ec965f9d3b610b839e652f4e4983363885f..ad3f4e0a59b4d8e688f97ac7b76eb8b3243a1531 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -24,7 +24,7 @@ Section case.
     iDestruct "Hown" as (i vl' vl'') "(>% & >EQlen & Hown)". subst.
     simpl ty_size. iDestruct "EQlen" as %[=EQlen]. rewrite -EQlen. simpl length.
     rewrite -Nat.add_1_l app_length -!freeable_sz_split
-            heap_mapsto_vec_cons heap_mapsto_vec_app.
+            heap_pointsto_vec_cons heap_pointsto_vec_app.
     iDestruct "H↦" as "(H↦i & H↦vl' & H↦vl'')".
     iDestruct "Hf" as "(Hfi & Hfvl' & Hfvl'')".
     rewrite nth_lookup.
@@ -35,13 +35,13 @@ Section case.
       rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //=; iFrame "HT".
     - rewrite /own_ptr /=. iDestruct (ty.(ty_size_eq) with "Hown") as %<-.
       iSplitL "H↦i Hfi"; last iSplitR "H↦vl'' Hfvl''".
-      + rewrite shift_loc_0. iFrame. iExists [ #i]. rewrite heap_mapsto_vec_singleton.
+      + rewrite shift_loc_0. iFrame. iExists [ #i]. rewrite heap_pointsto_vec_singleton.
         iFrame. auto.
       + eauto with iFrame.
       + rewrite -EQlen app_length Nat.add_comm Nat.add_sub shift_loc_assoc Nat2Z.id.
         iFrame. iExists _. iFrame. auto.
     - rewrite /= -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
-      iExists (#i :: vl' ++ vl''). iNext. rewrite heap_mapsto_vec_cons heap_mapsto_vec_app.
+      iExists (#i :: vl' ++ vl''). iNext. rewrite heap_pointsto_vec_cons heap_pointsto_vec_app.
       iFrame. iExists i, vl', vl''. rewrite /= app_length nth_lookup EQty /=. auto.
   Qed.
 
@@ -73,7 +73,7 @@ Section case.
     iDestruct "H↦" as (vl) "[H↦ Hown]".
     iDestruct "Hown" as (i vl' vl'') "(>% & >EQlen & Hown)". subst.
     iDestruct "EQlen" as %[=EQlen].
-    rewrite heap_mapsto_vec_cons heap_mapsto_vec_app nth_lookup.
+    rewrite heap_pointsto_vec_cons heap_pointsto_vec_app nth_lookup.
     iDestruct "H↦" as "(H↦i & H↦vl' & H↦vl'')".
     destruct (tyl !! i) as [ty|] eqn:EQty; last iDestruct "Hown" as ">[]".
     edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
@@ -85,7 +85,7 @@ Section case.
       { iIntros "!>Hown". iDestruct "Hown" as (vl'2) "[H↦ Hown]".
         iExists (#i::vl'2++vl''). iIntros "!>". iNext.
         iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'2.
-        rewrite heap_mapsto_vec_cons heap_mapsto_vec_app EQlenvl' EQlenvl'2.
+        rewrite heap_pointsto_vec_cons heap_pointsto_vec_app EQlenvl' EQlenvl'2.
         iFrame. iExists _, _, _. iSplit. { by auto. }
         rewrite /= -EQlen !app_length EQlenvl' EQlenvl'2 nth_lookup EQty /=. auto. }
       { iExists vl'. iFrame. }
@@ -96,7 +96,7 @@ Section case.
     - iMod ("Hclose'" with "[] [H↦i H↦vl' H↦vl'' Hown]") as "[Hb Htok]";
         [by iIntros "!>$"| |].
       { iExists (#i::vl'++vl'').
-        rewrite heap_mapsto_vec_cons heap_mapsto_vec_app /= -EQlen. iFrame. iNext.
+        rewrite heap_pointsto_vec_cons heap_pointsto_vec_app /= -EQlen. iFrame. iNext.
         iExists i, vl', vl''. rewrite nth_lookup EQty. auto. }
       iMod ("Hclose" with "Htok") as "HL".
       iDestruct ("HLclose" with "HL") as "HL".
@@ -163,7 +163,7 @@ Section case.
     iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
     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]".
+    rewrite heap_pointsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
     wp_write. wp_bind p1. iApply (wp_wand with "[]"); first by iApply (wp_eval_path).
     iIntros (? ->). wp_op. wp_bind p2. iApply (wp_hasty with "Hp2"); [done|].
     iIntros (v2 Hv2) "Hty2". iDestruct (ty_size_eq with "Hty2") as %Hlenty.
@@ -172,12 +172,12 @@ Section case.
       induction tyl as [|?? IHtyl]=>//= -[|i] /=.
       - intros [= ->]. simpl in *. lia.
       - apply IHtyl. simpl in *. lia. }
-    rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦vl" as "[H↦ H↦vl]". wp_write.
+    rewrite heap_pointsto_vec_cons -wp_fupd. iDestruct "H↦vl" as "[H↦ H↦vl]". wp_write.
     rewrite tctx_interp_singleton tctx_hasty_val' //.
     iMod ("Hw" with "[-HLclose]") as "[HL $]"; last first.
     { iApply "HLclose". done. }
     iNext.
-    iExists (_::_::_). rewrite !heap_mapsto_vec_cons. iFrame.
+    iExists (_::_::_). rewrite !heap_pointsto_vec_cons. iFrame.
     iExists i, [_], _. rewrite -Hlen nth_lookup Hty. auto.
   Qed.
 
@@ -206,11 +206,11 @@ Section case.
     iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
     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 -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl]".
+    rewrite heap_pointsto_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl]".
     wp_write. rewrite tctx_interp_singleton tctx_hasty_val' //.
     iMod ("Hw" with "[-HLclose]") as "[HL $]"; last first.
     { iApply "HLclose". done. }
-    iModIntro. iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame.
+    iModIntro. iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame.
     iExists i, [], _. rewrite -Hlen nth_lookup Hty. auto.
   Qed.
 
@@ -244,7 +244,7 @@ Section case.
     rewrite typed_write_eq in Hw.
     iMod (Hw with "[] LFT HE HL1 Hty1") as (l1 vl1) "(H & H↦ & Hw)"=>//=.
     clear Hw. destruct vl1 as [|? vl1]; iDestruct "H" as %[[= Hlen] ->].
-    rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl1]". wp_write.
+    rewrite heap_pointsto_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl1]". wp_write.
     wp_bind p1. iApply (wp_wand with "[]"); first by iApply (wp_eval_path). iIntros (? ->).
     wp_op. wp_bind p2. iApply (wp_hasty with "Hp2"); [done|]. iIntros (v2 Hv2) "Hty2".
     rewrite typed_read_eq in Hr.
@@ -253,7 +253,7 @@ Section case.
     { revert i Hty. rewrite Hlen. clear. induction tyl as [|?? IHtyl]=>//= -[|i] /=.
       - intros [= ->]. lia.
       - specialize (IHtyl i). intuition lia. }
-    rewrite -(take_drop (ty.(ty_size)) vl1) heap_mapsto_vec_app.
+    rewrite -(take_drop (ty.(ty_size)) vl1) heap_pointsto_vec_app.
     iDestruct "H↦vl1" as "[H↦vl1 H↦pad]".
     iDestruct (ty_size_eq with "Hty") as "#>%".
     iApply (wp_memcpy with "[$H↦vl1 $H↦2]"); [done| |lia|].
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 027962ae665a63c2e61a2af4f2c053c52b929aa7..e5e2c9f30a87133a154a75447b5fe22921e4e088 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -24,7 +24,7 @@ Section uniq_bor.
     iMod (bor_exists with "LFT Hshr") as ([|[[|l'|]|][]]) "Hb"; first solve_ndisj;
       (iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]"; first solve_ndisj);
       try (iMod (bor_persistent with "LFT Hb2 Htok") as "[>[] _]"; solve_ndisj).
-    iFrame. iExists l'. rewrite heap_mapsto_vec_singleton.
+    iFrame. iExists l'. rewrite heap_pointsto_vec_singleton.
     iMod (bor_fracture (l ↦{1} #l')%I with "LFT Hb1") as "$"; first solve_ndisj.
     iApply delay_sharing_nested; try done. iApply lft_incl_refl.
   Qed.