diff --git a/heap.v b/heap.v
index 72e6f366cceccd04b463e0d942b0a4076bfa3ce1..3088e4533c2f04d44f4a89f955a408a5b4766a96 100644
--- a/heap.v
+++ b/heap.v
@@ -146,7 +146,7 @@ Section heap.
     l ↦★{q} (vl1 ++ vl2) ⊣⊢ l ↦★{q} vl1 ★ shift_loc l (length vl1) ↦★{q} vl2.
   Proof.
     rewrite /heap_mapsto_vec big_sepL_app.
-    do 2 f_equiv. intros k v. by rewrite shift_loc_assoc Nat2Z.inj_add.
+    do 2 f_equiv. intros k v. by rewrite shift_loc_assoc_nat.
   Qed.
 
   Lemma heap_mapsto_vec_singleton l q v : l ↦★{q} [v] ⊣⊢ l ↦{q} v.
@@ -213,12 +213,12 @@ Section heap.
       { simpl. by rewrite /= right_id shift_loc_0 heap_mapsto_eq. }
       iSplitL "Hv"; first by rewrite shift_loc_0 heap_mapsto_eq.
       erewrite imap_ext; [done|]. intros k v'' _; simpl.
-      by rewrite shift_loc_assoc Z.add_1_l -Nat2Z.inj_succ.
+      by rewrite (shift_loc_assoc_nat _ 1).
     -iIntros "[%|[Hv Hvl]]"; simplify_eq.
      iSplitL "Hv"; first by rewrite shift_loc_0 heap_mapsto_eq.
      destruct vl as [|v' vl]; first eauto.
      iRight. erewrite imap_ext; [done|]. intros k v'' _; simpl.
-     by rewrite shift_loc_assoc Z.add_1_l -Nat2Z.inj_succ.
+     by rewrite (shift_loc_assoc_nat _ 1).
   Qed.
 
   Lemma inter_lookup_Some i j (n:nat):
@@ -307,8 +307,8 @@ Section heap.
     - rewrite imap_cons. simpl. etrans. apply (IH (shift_loc l 1)).
       { intros. by rewrite shift_loc_assoc. }
       rewrite auth_frag_op assoc. apply cmra_update_op; last first.
-      { erewrite imap_ext. reflexivity. move=>i x/= _. rewrite shift_loc_assoc.
-        f_equal. f_equal. lia. }
+      { erewrite imap_ext. reflexivity. move=>i x/= _.
+        by rewrite (shift_loc_assoc_nat _ 1). }
       assert (Hinit: (to_heapVal (init_mem (shift_loc l 1) vl σ)) !! l = None).
       { clear-FRESH. rewrite lookup_fmap fmap_None.
         cut (0 < 1); last lia. generalize 1. revert l FRESH.
@@ -349,7 +349,7 @@ Section heap.
         * specialize (FRESH (i-l.2)). rewrite /shift_loc Zplus_minus in FRESH.
           rewrite lookup_empty FRESH. by split; intros []%is_Some_None.
         * rewrite !lookup_insert_is_Some IH /=;
-                  last by intros; rewrite shift_loc_assoc.
+            last by intros; rewrite shift_loc_assoc.
           destruct l. simpl. split; intros [|[]]; naive_solver congruence.
     - rewrite lookup_op lookup_insert_ne // lookup_empty.
       specialize (REL blk). revert REL. case: (h !! blk); last inversion 2.
@@ -405,7 +405,7 @@ Section heap.
     induction vl as [|v vl IH]=>l. by rewrite left_id.
     rewrite imap_cons /= auth_frag_op -assoc. etrans.
     - apply cmra_update_op. reflexivity. erewrite imap_ext. apply (IH (shift_loc l 1)).
-      move=> i x /= _. rewrite shift_loc_assoc. repeat f_equiv. lia.
+      move=> i x /= _. by rewrite (shift_loc_assoc_nat _ 1).
     - clear IH. unfold to_heapVal. rewrite fmap_delete.
       apply cmra_update_valid0. intros [[f Hf%timeless] Hv]; last apply _.
       revert Hf Hv. rewrite shift_loc_0 right_id =>/= Hf. rewrite {1 2}Hf=>Hv.
diff --git a/lang.v b/lang.v
index db34326b54db89d9f2e05272a65bc4f2ef9fe5a9..37f9f111513b444e17e25add85a29c2c17fb776f 100644
--- a/lang.v
+++ b/lang.v
@@ -340,6 +340,13 @@ Lemma shift_loc_0:
   ∀ l, shift_loc l 0 = l.
 Proof. unfold shift_loc=>[[??]] /=. f_equal. lia. Qed.
 
+Lemma shift_loc_assoc_nat:
+  ∀ l (n n' : nat), shift_loc (shift_loc l n) n' = shift_loc l (n+n')%nat.
+Proof. unfold shift_loc=>/= l n n'. f_equal. lia. Qed.
+Lemma shift_loc_0_nat:
+  ∀ l, shift_loc l 0%nat = l.
+Proof. unfold shift_loc=>[[??]] /=. f_equal. lia. Qed.
+
 Definition fresh_block (σ : state) : block :=
   let blocklst := (elements (dom _ σ : gset loc)).*1 in
   let blockset : gset block := foldr (fun b s => {[b]} ∪ s)%C ∅ blocklst in
diff --git a/perm_incl.v b/perm_incl.v
index f28a5847302ec66a0a0f6aede7ba6cac0d24a32a..b6e1e1e20666031c8ea8b85193213e8ce8c0f9eb 100644
--- a/perm_incl.v
+++ b/perm_incl.v
@@ -57,6 +57,9 @@ Section props.
     iVs (B with "A") as "$". iApply (D with "B").
   Qed.
 
+  Lemma uPred_equiv_perm_equiv ρ θ : (∀ tid, ρ tid ⊣⊢ θ tid) → (ρ ⇔ θ).
+  Proof. intros Heq. split=>tid; rewrite Heq; by iIntros. Qed.
+
   Lemma perm_incl_top ρ : ρ ⇒ ⊤.
   Proof. iIntros (tid) "H". eauto. Qed.
 
@@ -111,67 +114,74 @@ Section props.
     iExists _. iSplit. done. done.
   Admitted.
 
+  Lemma split_own_prod tyl (q0: Qp) (ql : list Qp) (l : loc) tid :
+    length tyl = length ql →
+      (own (foldr Qp_plus q0 ql) (product tyl)).(ty_own) tid [ #l] ⊣⊢
+    ▷ †{q0}(shift_loc l (0 + (product tyl).(ty_size))%nat)…0 ★
+    [★ list] qtyoffs ∈ (combine ql (combine_offs tyl 0)),
+         (own (qtyoffs.1) (qtyoffs.2.1)).(ty_own)
+              tid [ #(shift_loc l (qtyoffs.2.2))].
+  Proof.
+    intros Hlen.
+    assert (REW: ∀ (l : loc) (Φ : loc → iProp Σ),
+               Φ l ⊣⊢ (∃ l0:loc, [ #l] = [ #l0] ★ Φ l0)).
+    { intros l0 Φ. iSplit; iIntros "H". eauto.
+      iDestruct "H" as (l') "[Heq H]". iDestruct "Heq" as %[=]. subst. done. }
+    setoid_rewrite <-REW. clear REW.
+    rewrite big_sepL_sepL assoc split_prod_mt big_sepL_later. apply uPred.sep_proper.
+    - rewrite -{1}(shift_loc_0_nat l). generalize 0%nat at -3. revert ql Hlen.
+      induction tyl as [|ty tyl IH]; intros [|q ql] [=] offs.
+      + by rewrite big_sepL_nil !right_id.
+      + rewrite -heap_freeable_op_eq uPred.later_sep shift_loc_assoc_nat IH //
+                Nat.add_assoc big_sepL_cons.
+        iSplit; by iIntros "($&$&$)".
+    - generalize 0%nat. revert ql Hlen.
+      induction tyl as [|ty tyl IH]; intros [|q ql] [=] offs. done.
+      rewrite !big_sepL_cons IH //.
+  Qed.
+
   Lemma perm_split_own_prod tyl (q : Qp) (ql : list Qp) v :
     length tyl = length ql →
     foldr (λ (q : Qp) acc, q + acc)%Qc 0%Qc ql = q →
     v ◁ own q (product tyl) ⇔
-      foldr (λ qtysz acc,
-             proj_valuable (Z.of_nat (qtysz.2.2)) v ◁
-                           own (qtysz.1) (qtysz.2.1) ★ acc)
+      foldr (λ qtyoffs acc,
+             proj_valuable (Z.of_nat (qtyoffs.2.2)) v ◁
+                           own (qtyoffs.1) (qtyoffs.2.1) ★ acc)
             ⊤ (combine ql (combine_offs tyl 0)).
   Proof.
-    destruct tyl as [|ty0 tyl], ql as [|q0 ql]; try done.
-    { simpl. intros _?. destruct q as [q ?]. simpl in *. by subst. }
-    destruct v as [[[|l|]|]|];
-      try by split; iIntros (tid) "H";
-        [iDestruct "H" as (l) "[% _]" || iDestruct "H" as "[]" |
-         iDestruct "H" as "[[]_]"].
-    intros [= EQ]. revert EQ.
-    rewrite -{1}(shift_loc_0 l). change 0 with (Z.of_nat 0). generalize O at 2 3.
-    revert q ty0 q0 ql. induction tyl as [|ty1 tyl IH]=>q ty0 q0 ql offs Hlen Hq;
-      destruct ql as [|q1 ql]; try done.
-    - simpl in Hq. rewrite ->Qcplus_0_r, <-Qp_eq in Hq. subst q.
-      rewrite /= right_id. split; iIntros (tid) "H!==>/="; rewrite Nat.add_0_r.
-      + iDestruct "H" as (l') "(%&?&H)". iExists l'. iSplit. done. iFrame. iNext.
-        iDestruct "H" as (vl) "[Hvl H]".
-        iDestruct "H" as ([|?[|??]]) "(%&%&?)"; try done.
-        iExists _. subst. rewrite /= app_nil_r big_sepL_singleton. by iFrame.
-      + iDestruct "H" as (l') "(%&?&Hown)". iExists l'. iSplit. done. iFrame. iNext.
-        iDestruct "Hown" as (vl) "[Hmt Hown]". iExists vl. iFrame.
-        iExists [vl]. rewrite /= app_nil_r big_sepL_singleton. iFrame. by iSplit.
-    - assert (Hq' : (0 < q1 + foldr (λ (q : Qp) acc, q + acc) 0 ql)%Qc).
-      { apply Qcplus_pos_nonneg. done. clear. induction ql. done.
-        apply Qcplus_nonneg_nonneg; last done. by apply Qclt_le_weak. }
-      pose (q' := mk_Qp _ Hq').
-      assert (q = q0 + q')%Qp as -> by rewrite Qp_eq -Hq //. clear Hq.
-      injection Hlen. clear Hlen. intro Hlen.
-      simpl in IH|-*. rewrite -(IH q') //. clear IH. split; iIntros (tid) "H".
-      + iDestruct "H" as (l') "(Hl'&Hf&H)". iDestruct "Hl'" as %[= Hl']. subst.
-        iDestruct "H" as (vl) "[Hvl H]".
-        iDestruct "H" as ([|vl0[|vl1 vll]]) "(>%&>%&Hown)"; try done. subst.
-        rewrite big_sepL_cons heap_mapsto_vec_app -heap_freeable_op_eq.
-        iDestruct "Hf" as "[Hf0 Hfq]". iDestruct "Hvl" as "[Hvl0 Hvll]".
-        iDestruct "Hown" as "[Hown0 Hown]".
-        iAssert (▷ (length vl0 = ty_size ty0))%I with "[#]" as "#>Hlenvl0".
-        { iNext. iApply (ty_size_eq with "Hown0"). }
-        iDestruct "Hlenvl0" as %Hlenvl0. iVsIntro. iSplitL "Hf0 Hvl0 Hown0".
-        * iExists _. iSplit. done. iFrame. iNext. iExists vl0. by iFrame.
-        * iExists _. iSplit. done. rewrite !shift_loc_assoc -!Nat2Z.inj_add Hlenvl0.
-          iFrame. iNext. iExists (concat (vl1 :: vll)). iFrame. iExists (_ :: _).
-          iSplit. done. iFrame. iPureIntro. simpl in *. congruence.
-      + iDestruct "H" as "[H0 H]".
-        iDestruct "H0" as (vl0) "(Heq&Hf0&Hmt0)". iDestruct "Heq" as %[= ?]. subst vl0.
-        iDestruct "H" as (vl) "(Heq&Hf&Hmt)". iDestruct "Heq" as %[= ?]. subst vl.
-        iVsIntro. iExists (shift_loc l offs). iSplit. done. iNext.
-        iSplitL "Hf Hf0".
-        * rewrite -heap_freeable_op_eq shift_loc_assoc Nat2Z.inj_add. by iFrame.
-        * iDestruct "Hmt0" as (vl0) "[Hmt0 Hown0]". iDestruct "Hmt" as (vl) "[Hmt Hown]".
-          iDestruct (ty_size_eq with "Hown0") as %<-.
-          iExists (vl0 ++ vl). iSplitL "Hmt Hmt0".
-          { rewrite heap_mapsto_vec_app shift_loc_assoc Nat2Z.inj_add. by iFrame. }
-          iDestruct "Hown" as (vll) "(%&%&Hown)". subst.
-          iExists (_ :: _). iSplit. done. iSplit. iPureIntro; simpl in *; congruence.
-          rewrite big_sepL_cons. by iFrame.
+    intros Hlen Hq.
+    assert (DEC : Decision (∃ (l : loc), v = Some #l)).
+    { destruct v as [[[]|]|]; try by right; intros [l [=]]. left; eauto. }
+    destruct DEC as [[l ->]|Hv]; last first.
+    { destruct tyl as [|ty0 tyl], ql as [|q0 ql]; try done.
+      { destruct q as [q ?]. simpl in *. by subst. }
+      destruct v as [[[|l|]|]|];
+        try by split; iIntros (tid) "H";
+          [iDestruct "H" as (l) "[% _]" || iDestruct "H" as "[]" |
+           iDestruct "H" as "[[]_]"].
+      naive_solver. }
+    destruct (@exists_last _ ql) as (ql'&q0&->).
+    { destruct ql as [|q0 ql]; last done. destruct q. simpl in *. by subst. }
+    assert (foldr Qp_plus (q0/2) (ql' ++ [q0/2]) = q)%Qp as <-.
+    { destruct q as [q Hqpos]. apply Qp_eq. simpl in *. subst. clear. induction ql'.
+      - by rewrite /fold_right /app Qp_div_2 Qcplus_0_r.
+      - by rewrite /= IHql'. }
+    revert Hlen. assert (length (ql' ++ [q0]) = length (ql' ++ [q0/2]%Qp)) as ->. 
+    { rewrite !app_length /=. lia. }
+    intros Hlen. apply uPred_equiv_perm_equiv=>tid.
+    rewrite /has_type /from_option split_own_prod //.
+    clear -Hlen. revert ql' Hlen. generalize 0%nat at -2.
+    induction tyl as [|ty tyl IH]; destruct ql' as [|q ql']=>Hlen; try done.
+    - destruct tyl; last done. clear IH Hlen.
+      rewrite big_sepL_singleton /= /sep !right_id comm uPred.sep_exist_r.
+      apply uPred.exist_proper=>l0.
+      rewrite -{3}(Qp_div_2 q0) -{3}(right_id O plus ty.(ty_size))
+              -heap_freeable_op_eq uPred.later_sep -!assoc.
+      iSplit; iIntros "[#Eq [? [? ?]]]"; iFrame "# ★";
+        iDestruct "Eq" as %[=]; subst; rewrite shift_loc_assoc_nat //.
+    - simpl in *. rewrite big_sepL_cons /sep -IH; last by congruence. clear IH.
+      rewrite !uPred.sep_exist_r !uPred.sep_exist_l. apply uPred.exist_proper=>l0.
+      rewrite -!assoc /=. by iSplit; iIntros "[$[$[$[$$]]]]".
   Qed.
 
 End props.
diff --git a/type.v b/type.v
index 3e916c8d1ce45f355c8cd7aa0d281f91641fd681..cc76ef17962828cad95626327b95019664305fb8 100644
--- a/type.v
+++ b/type.v
@@ -287,8 +287,8 @@ Section types.
     ⊣⊢ [★ list] tyoffs ∈ combine_offs tyl 0,
          shift_loc l (tyoffs.2) ↦★{q}: ty_own (tyoffs.1) tid.
   Proof.
-    rewrite -{1}(shift_loc_0 l). change 0%Z with (Z.of_nat 0).
-    generalize 0%nat. induction tyl as [|ty tyl IH]=>/= offs.
+    rewrite -{1}(shift_loc_0_nat l). generalize 0%nat.
+    induction tyl as [|ty tyl IH]=>/= offs.
     - iSplit; iIntros "_". by iApply big_sepL_nil.
       iExists []. iSplit. by iApply heap_mapsto_vec_nil.
       iExists []. repeat iSplit; try done. by iApply big_sepL_nil.
@@ -301,12 +301,12 @@ Section types.
         iDestruct (ty.(ty_size_eq) with "Hownh") as %->.
         iSplitL "Hmth Hownh". iExists vl0. by iFrame.
         iExists (concat vll). iSplitL "Hmtq"; last by eauto.
-        by rewrite shift_loc_assoc Nat2Z.inj_add.
+        by rewrite shift_loc_assoc_nat.
       + iIntros "[Hmth H]". iDestruct "H" as (vl) "[Hmtq H]".
         iDestruct "H" as (vll) "(%&Hlen&Hownq)". subst.
         iDestruct "Hmth" as (vlh) "[Hmth Hownh]". iDestruct "Hlen" as %->.
         iExists (vlh ++ concat vll).
-        rewrite heap_mapsto_vec_app shift_loc_assoc Nat2Z.inj_add.
+        rewrite heap_mapsto_vec_app shift_loc_assoc_nat.
         iDestruct (ty.(ty_size_eq) with "Hownh") as %->. iFrame.
         iExists (vlh :: vll). rewrite big_sepL_cons. iFrame. auto.
   Qed.