diff --git a/theories/perm.v b/theories/perm.v
index e268dacdf8cabb6f12732909ad20ccad03105779..52f9eb2e343be0d85746bf078012996caee17f88 100644
--- a/theories/perm.v
+++ b/theories/perm.v
@@ -51,7 +51,7 @@ End Perm.
 
 Import Perm.
 
-Notation "v ◁ ty" := (has_type v ty)
+Notation "ν ◁ ty" := (has_type ν%E ty)
   (at level 75, right associativity) : perm_scope.
 
 Notation "κ ∋ ρ" := (extract κ ρ)
diff --git a/theories/perm_incl.v b/theories/perm_incl.v
index cca2d892ba399fdc1f6933b9a4838a163c885eb8..d236d6bde8ea484ad879cd4ce0c1e90222806efc 100644
--- a/theories/perm_incl.v
+++ b/theories/perm_incl.v
@@ -109,86 +109,129 @@ Section props.
     destruct (eval_expr ν); last by iDestruct "Huniq" as "[]".
     iDestruct "Huniq" as (l) "[% Hown]".
     iMod (ty.(ty_share) _ lrustN with "Hown Htok") as "[Hown $]".
-    apply disjoint_union_l; solve_ndisj. done. iModIntro.
-    simpl. eauto.
+    apply disjoint_union_l; solve_ndisj. done. iIntros "!>/=". eauto.
   Qed.
 
-  Lemma split_own_prod tyl (q0: Qp) (ql : list Qp) (l : loc) tid :
-    length tyl = length ql →
-      (own (foldr Qp_plus q0 ql) (Π tyl)).(ty_own) tid [ #l] ⊣⊢
-    ▷ †{q0}(shift_loc l (0 + (Π 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))].
+  Lemma perm_split_own_prod2 ty1 ty2 (q1 q2 : Qp) ν :
+    ν ◁ own (q1 + q2) (product2 ty1 ty2) ⇔
+      ν ◁ own q1 ty1 ∗ ν +ₗ #ty1.(ty_size) ◁ own q2 ty2.
   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 //.
+    rewrite /has_type /own /sep /=.
+    destruct (eval_expr ν) as [[[]|?]|]; last first; split; iIntros (tid) "H/=";
+      (try by iDestruct "H" as "[_ []]"); (try by iDestruct "H" as (l) "[% _]").
+    { by auto. }
+    - iDestruct "H" as (l') "(EQ & H & H†)". iDestruct "EQ" as %[=<-].
+      iDestruct "H" as (vl) "[H↦ H]". iDestruct "H" as (vl1 vl2) "(>% & H1 & H2)".
+      subst. rewrite heap_mapsto_vec_app -heap_freeable_op_eq.
+      iDestruct "H†" as "[H†1 H†2]". iDestruct "H↦" as "[H↦1 H↦2]".
+      iAssert (â–· (length vl1 = ty_size ty1))%I with "[#]" as ">EQ".
+      { iNext. by iApply ty_size_eq. }
+      iDestruct "EQ" as %->. iSplitL "H↦1 H†1 H1".
+      + iExists _. iSplitR. done. iFrame. iExists _. by iFrame.
+      + iExists _. iSplitR. done. iFrame. iExists _. by iFrame.
+    - iDestruct "H" as "[H1 H2]".
+      iDestruct "H1" as (l') "(EQ & H↦1 & H†1)". iDestruct "EQ" as %[=<-].
+      iDestruct "H2" as (l') "(EQ & H↦2 & H†2)". iDestruct "EQ" as %[=<-].
+      iExists l. iSplitR. done. rewrite -heap_freeable_op_eq. 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.
+      iAssert (â–· (length vl1 = ty_size ty1))%I with "[#]" as ">EQ".
+      { iNext. by iApply ty_size_eq. }
+      iDestruct "EQ" as %->. iFrame. iExists vl1, vl2. iFrame. auto.
   Qed.
 
+  Fixpoint combine_offs (tyl : list type) (accu : nat) :=
+    match tyl with
+    | [] => []
+    | ty :: q => (ty, accu) :: combine_offs q (accu + ty.(ty_size))
+    end.
+
   Lemma perm_split_own_prod tyl (q : Qp) (ql : list Qp) ν :
     length tyl = length ql →
     foldr (λ (q : Qp) acc, q + acc)%Qc 0%Qc ql = q →
     ν ◁ own q (Π tyl) ⇔
       foldr (λ qtyoffs acc,
-             (ν +ₗ #(qtyoffs.2.2:nat))%E ◁ own (qtyoffs.1) (qtyoffs.2.1) ∗ acc)
+             ν +ₗ #(qtyoffs.2.2:nat) ◁ own (qtyoffs.1) (qtyoffs.2.1) ∗ acc)
             ⊤ (combine ql (combine_offs tyl 0)).
   Proof.
-    intros Hlen Hq. assert (ql ≠ []).
-    { destruct ql as [|q0 ql]; last done. destruct q. simpl in *. by subst. }
-    unfold has_type. simpl eval_expr. destruct (eval_expr ν) as [[[|l|]|]|];
-      try by (destruct tyl as [|ty0 tyl], ql as [|q0 ql]; try done;
-        by split; iIntros (tid) "H"; try done;
-          [iDestruct "H" as (l) "[% _]" || iDestruct "H" as "[]" |
-           iDestruct "H" as "[[]_]"]).
-    destruct (@exists_last _ ql) as (ql'&q0&->); first done.
-    apply uPred_equiv_perm_equiv=>tid.
-    assert (foldr Qp_plus (q0/2) (ql' ++ [q0/2]) = q)%Qp as <-.
-    { destruct q as [q ?]. apply Qp_eq. simpl in *. subst. clear. induction ql'.
-      by rewrite /fold_right /app Qp_div_2 Qcplus_0_r. by rewrite /= IHql'. }
-    rewrite /has_type /from_option split_own_prod ?Hlen ?app_length //.
-    clear -Hlen. revert ql' Hlen. generalize 0%nat at -2.
-    induction tyl as [|ty tyl IH]; destruct ql' as [|q ql']; intros [= 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 //.
-    - rewrite /= big_sepL_cons /sep -IH // !uPred.sep_exist_r uPred.sep_exist_l.
-      apply uPred.exist_proper=>l0. rewrite -!assoc /=.
-      by iSplit; iIntros "[$[$[$[$$]]]]".
+    revert q tyl ν. induction ql as [|q0 [|q1 ql] IH]=>q tyl ν Hlen Hq.
+    { destruct q. intros. simpl in *. by subst. }
+    - destruct tyl as [|ty0 [|ty1 tyl]]; try done. simpl in *.
+      assert (q0 = q) as ->. { apply Qp_eq. by rewrite -Hq Qcplus_0_r. }
+      rewrite /has_type /sep /=.
+      destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "H/=";
+        (try by iDestruct "H" as "[[] _]"); (try by iDestruct "H" as (l) "[% _]");
+        (try by auto); rewrite (shift_loc_0 l) Nat.add_0_r.
+      + iSplitL; last done. iExists _. iSplitR. done.
+        iDestruct "H" as (l') "[Heq [H↦ H†]]". iDestruct "Heq" as %[=<-].
+        iDestruct "H↦" as (vl) "[H↦ H]".
+        iDestruct "H" as (vl1 vl2) "(>% & Hown & >%)". subst.
+        rewrite app_nil_r. iFrame. iExists _. by iFrame.
+      + iExists l. iSplitR. done.
+        iDestruct "H" as "[H _]". iDestruct "H" as (l') "[Heq [H↦ H†]]".
+        iDestruct "Heq" as %[=<-]. iFrame. iDestruct "H↦" as (vl) "[H↦ Hown]".
+        iExists vl. iFrame. iExists vl, []. iFrame. rewrite app_nil_r. auto.
+    - destruct tyl as [|ty0 tyl]. done.
+      assert (Hpos : (0 < foldr (λ (q : Qp) acc, (q + acc)%Qc) 0%Qc (q1 :: ql))%Qc).
+      { apply Qcplus_pos_nonneg. apply Qp_prf. clear. induction ql. done.
+        apply Qcplus_nonneg_nonneg. apply Qclt_le_weak, Qp_prf. done. }
+      assert (q = q0 + mk_Qp _ Hpos)%Qp as ->. by by apply Qp_eq; rewrite -Hq.
+      injection Hlen; intro Hlen'. rewrite perm_split_own_prod2 IH //.
+      apply perm_sep_proper.
+      + rewrite /has_type /sep /=.
+        destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "H/=";
+        (try by iDestruct "H" as "[]"); (try by iDestruct "H" as (l) "[% _]");
+        (try by auto); by rewrite shift_loc_0.
+      + cut (length tyl = length (q1 :: ql)); last done. clear. revert tyl.
+        generalize 0%nat. induction (q1 :: ql)=>offs -[|ty tyl] Hlen //.
+        apply perm_sep_proper.
+        * rewrite /has_type /sep /=.
+          destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "H/=";
+          (try by iDestruct "H" as "[]"); (try by iDestruct "H" as (l) "[% _]");
+          (try by auto); by rewrite shift_loc_assoc_nat (comm plus).
+        * etransitivity. apply IHl. by injection Hlen. do 3 f_equiv. lia.
+  Qed.
+
+  Lemma perm_split_uniq_borrow_prod2 ty1 ty2 κ ν :
+    ν ◁ &uniq{κ} (product2 ty1 ty2) ⇒
+    ν ◁ &uniq{κ} ty1 ∗ ν +ₗ #(ty1.(ty_size)) ◁ &uniq{κ} ty2.
+  Proof.
+    rewrite /has_type /sep /product2 /=.
+    destruct (eval_expr ν) as [[[|l|]|]|];
+      iIntros (tid) "H"; try iDestruct "H" as "[]";
+        iDestruct "H" as (l0) "[EQ H]"; iDestruct "EQ" as %[=<-].
+    rewrite /= split_prod_mt. iMod (borrow_split with "H") as "[H1 H2]".
+    set_solver. iSplitL "H1"; eauto.
   Qed.
 
   Lemma perm_split_uniq_borrow_prod tyl κ ν :
     ν ◁ &uniq{κ} (Π tyl) ⇒
       foldr (λ tyoffs acc,
-             (ν +ₗ #(tyoffs.2:nat))%E ◁ &uniq{κ} (tyoffs.1) ∗ acc)%P
+             ν +ₗ #(tyoffs.2:nat) ◁ &uniq{κ} (tyoffs.1) ∗ acc)%P
             ⊤ (combine_offs tyl 0).
   Proof.
-    intros tid. unfold has_type. simpl eval_expr.
+    transitivity (ν +ₗ #0%nat ◁ &uniq{κ}Π tyl)%P.
+    { iIntros (tid) "H/=". rewrite /has_type /=. destruct (eval_expr ν)=>//.
+      iDestruct "H" as (l) "[Heq H]". iDestruct "Heq" as %[=->].
+      rewrite shift_loc_0 /=. eauto. }
+    generalize 0%nat. induction tyl as [|ty tyl IH]=>offs. by iIntros (tid) "H/=".
+    etransitivity. apply perm_split_uniq_borrow_prod2.
+    iIntros (tid) "/=[$ H]". iApply IH. rewrite /has_type /=.
+    destruct (eval_expr ν) as [[[]|]|]=>//=. by rewrite shift_loc_assoc_nat.
+  Qed.
+
+  Lemma perm_split_shr_borrow_prod2 ty1 ty2 κ ν :
+    ν ◁ &shr{κ} (product2 ty1 ty2) ⇒
+    ν ◁ &shr{κ} ty1 ∗ ν +ₗ #(ty1.(ty_size)) ◁ &shr{κ} ty2.
+  Proof.
+    rewrite /has_type /sep /product2 /=.
     destruct (eval_expr ν) as [[[|l|]|]|];
-      iIntros "H"; try iDestruct "H" as "[]";
-        iDestruct "H" as (l0) "[EQ H]"; iDestruct "EQ" as %[=]. subst l0.
-    rewrite split_prod_mt.
-    iInduction (combine_offs tyl 0) as [|[ty offs] ll] "IH". by auto.
-    rewrite big_sepL_cons /=.
-    iMod (borrow_split with "H") as "[H0 H]". set_solver.
-    iMod ("IH" with "H") as "$". iModIntro. iExists _. eauto.
+      iIntros (tid) "H"; try iDestruct "H" as "[]";
+        iDestruct "H" as (l0) "(EQ & H)"; iDestruct "EQ" as %[=<-].
+    iDestruct "H" as (E1 E2) "(% & H1 & H2)".
+    iSplitL "H1"; iExists _; (iSplitR; [done|]); iApply (ty_shr_mono with "[]");
+      try by iFrame.
+    set_solver. iApply lft_incl_refl. set_solver. iApply lft_incl_refl.
   Qed.
 
   Lemma perm_split_shr_borrow_prod tyl κ ν :
@@ -197,19 +240,15 @@ Section props.
              (ν +ₗ #(tyoffs.2:nat))%E ◁ &shr{κ} (tyoffs.1) ∗ acc)%P
             ⊤ (combine_offs tyl 0).
   Proof.
-    intros tid. unfold has_type. simpl eval_expr.
-    destruct (eval_expr ν) as [[[|l|]|]|];
-      iIntros "H"; try iDestruct "H" as "[]";
-        iDestruct "H" as (l0) "[EQ H]"; iDestruct "EQ" as %[=]. subst l0.
-    simpl. iModIntro.
-    change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat).
-    generalize O at 2; intro i.
-    iInduction (combine_offs tyl 0) as [|[ty offs] ll] "IH" forall (i). by auto.
-    rewrite big_sepL_cons /=. iDestruct "H" as "[H0 H]".
-    setoid_rewrite <-Nat.add_succ_comm. iDestruct ("IH" $! (S i) with "H") as "$".
-    iExists _. iSplit. done. admit.
-    (* FIXME : namespaces problem. *)
-  Admitted.
+    transitivity (ν +ₗ #0%nat ◁ &shr{κ}Π tyl)%P.
+    { iIntros (tid) "H/=". rewrite /has_type /=. destruct (eval_expr ν)=>//.
+      iDestruct "H" as (l) "[Heq H]". iDestruct "Heq" as %[=->].
+      rewrite shift_loc_0 /=. iExists _. by iFrame "∗%". }
+    generalize 0%nat. induction tyl as [|ty tyl IH]=>offs. by iIntros (tid) "H/=".
+    etransitivity. apply perm_split_shr_borrow_prod2.
+    iIntros (tid) "/=[$ H]". iApply IH. rewrite /has_type /=.
+    destruct (eval_expr ν) as [[[]|]|]=>//=. by rewrite shift_loc_assoc_nat.
+  Qed.
 
   Lemma reborrow_shr_perm_incl κ κ' ν ty :
     κ ⊑ κ' ∗ ν ◁ &shr{κ'}ty ⇒ ν ◁ &shr{κ}ty.
@@ -218,8 +257,7 @@ Section props.
     destruct (eval_expr ν) as [[[|l|]|]|];
       try by (iDestruct "Hκ'" as "[]" || iDestruct "Hκ'" as (l) "[% _]").
     iDestruct "Hκ'" as (l') "[EQ Hκ']". iDestruct "EQ" as %[=]. subst l'.
-    iModIntro. iExists _. iSplit. done.
-    by iApply (ty_shr_mono with "Hord Hκ'").
+    iModIntro. iExists _. iSplit. done. by iApply (ty_shr_mono with "Hord Hκ'").
   Qed.
 
   Lemma borrowing_perm_incl κ ρ ρ1 ρ2 θ :
@@ -235,7 +273,7 @@ Section props.
     iIntros (tid) "_ Hown". unfold has_type.
     destruct (eval_expr ν) as [[[|l|]|]|];
       try by (iDestruct "Hown" as "[]" || iDestruct "Hown" as (l) "[% _]").
-    iDestruct "Hown" as (l') "[EQ [Hf Hown]]". iDestruct "EQ" as %[=]. subst l'.
+    iDestruct "Hown" as (l') "[EQ [Hown Hf]]". iDestruct "EQ" as %[=]. subst l'.
     iApply (fupd_mask_mono lftN). done.
     iMod (borrow_create with "Hown") as "[Hbor Hext]". done.
     iSplitL "Hbor". by simpl; eauto.
diff --git a/theories/type.v b/theories/type.v
index b5d228ac3f12c37bfaad5202c9f5af8de07627bc..0e93d48f68a093116fedbe28db8dc2c8adf4ad1b 100644
--- a/theories/type.v
+++ b/theories/type.v
@@ -1,3 +1,4 @@
+From Coq Require Import Qcanon.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Export thread_local.
 From iris.program_logic Require Import hoare.
@@ -23,10 +24,10 @@ Context `{iris_typeG Σ}.
 Record type :=
   { ty_size : nat; ty_dup : bool;
     ty_own : thread_id → list val → iProp Σ;
-    ty_shr : lifetime → thread_id → namespace → loc → iProp Σ;
+    ty_shr : lifetime → thread_id → coPset → loc → iProp Σ;
 
     ty_dup_persistent tid vl : ty_dup → PersistentP (ty_own tid vl);
-    ty_shr_persistent κ tid N l : PersistentP (ty_shr κ tid N l);
+    ty_shr_persistent κ tid E l : PersistentP (ty_shr κ tid E l);
 
     ty_size_eq tid vl : ty_own tid vl ⊢ length vl = ty_size;
     (* The mask for starting the sharing does /not/ include the
@@ -40,13 +41,13 @@ Record type :=
        give any. *)
     ty_share E N κ l tid q : mgmtE ⊥ nclose N → mgmtE ⊆ E →
       &{κ} (l ↦∗: ty_own tid) ⊢ q.[κ] ={E}=∗ ty_shr κ tid N l ∗ q.[κ];
-    ty_shr_mono κ κ' tid N l :
-      κ' ⊑ κ ⊢ ty_shr κ tid N l → ty_shr κ' tid N l;
-    ty_shr_acc κ tid E N l q :
-      ty_dup → mgmtE ∪ nclose N ⊆ E →
-      ty_shr κ tid N l ⊢
-        q.[κ] ∗ tl_own tid N ={E}=∗ ∃ q', ▷l ↦∗{q'}: ty_own tid ∗
-           (▷l ↦∗{q'}: ty_own tid ={E}=∗ q.[κ] ∗ tl_own tid N)
+    ty_shr_mono κ κ' tid E E' l : E ⊆ E' →
+      κ' ⊑ κ ⊢ ty_shr κ tid E l -∗ ty_shr κ' tid E' l;
+    ty_shr_acc κ tid E F l q :
+      ty_dup → mgmtE ∪ F ⊆ E →
+      ty_shr κ tid F l ⊢
+        q.[κ] ∗ tl_own tid F ={E}=∗ ∃ q', ▷l ↦∗{q'}: ty_own tid ∗
+           (▷l ↦∗{q'}: ty_own tid ={E}=∗ q.[κ] ∗ tl_own tid F)
   }.
 Global Existing Instances ty_shr_persistent ty_dup_persistent.
 
@@ -82,11 +83,11 @@ Next Obligation.
   done. set_solver.
 Qed.
 Next Obligation.
-  iIntros (st κ κ' tid N l) "#Hord H". iDestruct "H" as (vl) "[Hf Hown]".
+  intros st κ κ' tid E E' l ?. iIntros "#Hord H". iDestruct "H" as (vl) "[Hf Hown]".
   iExists vl. iFrame. by iApply (frac_borrow_shorten with "Hord").
 Qed.
 Next Obligation.
-  intros st κ tid N E l q ??.  iIntros "#Hshr[Hlft $]".
+  intros st κ tid E F l q ??. iIntros "#Hshr[Hlft $]".
   iDestruct "Hshr" as (vl) "[Hf Hown]".
   iMod (frac_borrow_acc with "[] Hf Hlft") as (q') "[Hmt Hclose]";
     first set_solver.
@@ -119,7 +120,7 @@ Section types.
      we really need [False] to prove [ty_incl_emp]. *)
   Program Definition emp :=
     {| ty_size := 0; ty_dup := true;
-       ty_own tid vl := False%I; ty_shr κ tid N l := False%I |}.
+       ty_own tid vl := False%I; ty_shr κ tid E l := False%I |}.
   Next Obligation. iIntros (tid vl) "[]". Qed.
   Next Obligation.
     iIntros (????????) "Hb Htok".
@@ -127,7 +128,7 @@ Section types.
     iMod (borrow_split with "Hb") as "[_ Hb]". set_solver.
     iMod (borrow_persistent with "Hb Htok") as "[>[] _]". set_solver.
   Qed.
-  Next Obligation. iIntros (?????) "_ []". Qed.
+  Next Obligation. intros. iIntros "_ []". Qed.
   Next Obligation. intros. iIntros "[]". Qed.
 
   Program Definition unit : type :=
@@ -142,8 +143,6 @@ Section types.
     {| st_size := 1; st_own tid vl := (∃ z:Z, vl = [ #z ])%I |}.
   Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
 
-  (* TODO own and uniq_borrow are very similar. They could probably
-     somehow share some bits..  *)
   Program Definition own (q : Qp) (ty : type) :=
     {| ty_size := 1; ty_dup := false;
        ty_own tid vl :=
@@ -153,11 +152,10 @@ Section types.
 
             Since this assertion is timeless, this should not cause
             problems. *)
-         (∃ l:loc, vl = [ #l ] ∗ ▷ †{q}l…ty.(ty_size)
-                               ∗ ▷ l ↦∗: ty.(ty_own) tid)%I;
-       ty_shr κ tid N l :=
+         (∃ l:loc, vl = [ #l ] ∗ ▷ l ↦∗: ty.(ty_own) tid ∗ ▷ †{q}l…ty.(ty_size))%I;
+       ty_shr κ tid E l :=
          (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
-            ∀ q', □ (q'.[κ] ={mgmtE ∪ N, mgmtE}▷=∗ ty.(ty_shr) κ tid N l' ∗ q'.[κ]))%I
+            ∀ q', □ (q'.[κ] ={mgmtE ∪ E, mgmtE}▷=∗ ty.(ty_shr) κ tid E l' ∗ q'.[κ]))%I
     |}.
   Next Obligation. done. Qed.
   Next Obligation.
@@ -171,7 +169,7 @@ Section types.
     iMod (borrow_split with "Hb2") as "[EQ Hb2]". set_solver.
     iMod (borrow_persistent with "EQ Htok") as "[>% $]". set_solver. subst.
     rewrite heap_mapsto_vec_singleton.
-    iMod (borrow_split with "Hb2") as "[_ Hb2]". set_solver.
+    iMod (borrow_split with "Hb2") as "[Hb2 _]". set_solver.
     iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "Hb1") as "Hbf". set_solver.
     rewrite /borrow. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
     iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty κ tid N l')%I
@@ -190,14 +188,15 @@ Section types.
     - iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
   Qed.
   Next Obligation.
-    iIntros (_ ty κ κ' tid N l) "#Hκ #H". iDestruct "H" as (l') "[Hfb Hvs]".
+    intros _ ty κ κ' tid E E' l ?. iIntros "#Hκ #H". iDestruct "H" as (l') "[Hfb Hvs]".
     iExists l'. iSplit. by iApply (frac_borrow_shorten with "[]").
     iIntros (q') "!#Htok".
+    iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption.
     iMod (lft_incl_acc with "Hκ Htok") as (q'') "[Htok Hclose]". set_solver.
     iMod ("Hvs" $! q'' with "Htok") as "Hvs'".
     iIntros "!>". iNext. iMod "Hvs'" as "[Hshr Htok]".
     iMod ("Hclose" with "Htok"). iFrame.
-    by iApply (ty.(ty_shr_mono) with "Hκ").
+    iApply (ty.(ty_shr_mono) with "Hκ"); last done. done.
   Qed.
   Next Obligation. done. Qed.
 
@@ -205,10 +204,10 @@ Section types.
     {| ty_size := 1; ty_dup := false;
        ty_own tid vl :=
          (∃ l:loc, vl = [ #l ] ∗ &{κ} l ↦∗: ty.(ty_own) tid)%I;
-       ty_shr κ' tid N l :=
+       ty_shr κ' tid E l :=
          (∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
             ∀ q', □ (q'.[κ ⋅ κ']
-               ={mgmtE ∪ N, mgmtE}▷=∗ ty.(ty_shr) (κ⋅κ') tid N l' ∗ q'.[κ⋅κ']))%I
+               ={mgmtE ∪ E, mgmtE}▷=∗ ty.(ty_shr) (κ⋅κ') tid E l' ∗ q'.[κ⋅κ']))%I
     |}.
   Next Obligation. done. Qed.
   Next Obligation.
@@ -239,162 +238,110 @@ Section types.
     - iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
   Qed.
   Next Obligation.
-    iIntros (κ0 ty κ κ' tid N l) "#Hκ #H". iDestruct "H" as (l') "[Hfb Hvs]".
-    iAssert (κ0⋅κ' ⊑ κ0⋅κ) as "#Hκ0".
+    intros κ0 ty κ κ' tid E E' l ?. iIntros "#Hκ #H".
+    iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⋅κ' ⊑ κ0⋅κ) as "#Hκ0".
     { iApply lft_incl_lb. iSplit.
       - iApply lft_le_incl. by exists κ'.
       - iApply lft_incl_trans. iSplit; last done.
         iApply lft_le_incl. exists κ0. apply (comm _). }
     iExists l'. iSplit. by iApply (frac_borrow_shorten with "[]"). iIntros (q) "!#Htok".
+    iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption.
     iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]". set_solver.
     iMod ("Hvs" $! q' with "Htok") as "Hclose'".  iIntros "!>". iNext.
     iMod "Hclose'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
-    by iApply (ty_shr_mono with "Hκ0").
+    iApply (ty_shr_mono with "Hκ0"); last done. done.
   Qed.
   Next Obligation. done. Qed.
 
   Program Definition shared_borrow (κ : lifetime) (ty : type) : type :=
     {| st_size := 1;
-       st_own tid vl := (∃ l:loc, vl = [ #l ] ∗ ty.(ty_shr) κ tid lrustN l)%I |}.
+       st_own tid vl :=
+         (∃ (l:loc), vl = [ #l ] ∗ ty.(ty_shr) κ tid lrustN l)%I |}.
   Next Obligation.
     iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
   Qed.
 
-  Fixpoint combine_offs (tyl : list type) (accu : nat) :=
-    match tyl with
-    | [] => []
-    | ty :: q => (ty, accu) :: combine_offs q (accu + ty.(ty_size))
-    end.
-
-  Lemma list_ty_type_eq tid (tyl : list type) (vll : list (list val)) :
-    length tyl = length vll →
-    ([∗ list] tyvl ∈ combine tyl vll, ty_own (tyvl.1) tid (tyvl.2))
-      ⊢ length (concat vll) = sum_list_with ty_size tyl.
-  Proof.
-    revert vll; induction tyl as [|ty tyq IH]; destruct vll;
-      iIntros (EQ) "Hown"; try done.
-    rewrite big_sepL_cons app_length /=. iDestruct "Hown" as "[Hown Hownq]".
-    iDestruct (ty.(ty_size_eq) with "Hown") as %->.
-    iDestruct (IH with "[-]") as %->; auto.
-  Qed.
-
-  Lemma split_prod_mt tid tyl l q :
+  Lemma split_prod_mt tid ty1 ty2 q l :
     (l ↦∗{q}: λ vl,
-       ∃ vll, vl = concat vll ∗ length tyl = length vll
-         ∗ [∗ list] tyvl ∈ combine tyl vll, ty_own (tyvl.1) tid (tyvl.2))%I
-    ⊣⊢ [∗ list] tyoffs ∈ combine_offs tyl 0,
-         shift_loc l (tyoffs.2) ↦∗{q}: ty_own (tyoffs.1) tid.
-  Proof.
-    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.
-    - rewrite big_sepL_cons -IH. iSplit.
-      + iIntros "H". iDestruct "H" as (vl) "[Hmt H]".
-        iDestruct "H" as ([|vl0 vll]) "(%&Hlen&Hown)";
-          iDestruct "Hlen" as %Hlen; inversion Hlen; subst.
-        rewrite big_sepL_cons heap_mapsto_vec_app/=.
-        iDestruct "Hmt" as "[Hmth Hmtq]"; iDestruct "Hown" as "[Hownh Hownq]".
-        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_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_nat.
-        iDestruct (ty.(ty_size_eq) with "Hownh") as %->. iFrame.
-        iExists (vlh :: vll). rewrite big_sepL_cons. iFrame. auto.
-  Qed.
-
-  Fixpoint nat_rec_shift {A : Type} (x : A) (f : nat → A → A) (n0 n : nat) :=
-    match n with
-    | O => x
-    | S n => f n0 (nat_rec_shift x f (S n0) n)
-    end.
-
-  Lemma split_prod_namespace tid (N : namespace) n :
-    ∃ E, (tl_own tid N ⊣⊢ tl_own tid E
-                 ∗ nat_rec_shift True (λ i P, tl_own tid (N .@ i) ∗ P) 0%nat n)
-         ∧ (∀ i, i < 0 → nclose (N .@ i) ⊆ E)%nat.
+       ∃ vl1 vl2, vl = vl1 ++ vl2 ∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I
+       ⊣⊢ l ↦∗{q}: ty1.(ty_own) tid ∗ shift_loc l ty1.(ty_size) ↦∗{q}: ty2.(ty_own) tid.
   Proof.
-    generalize 0%nat. induction n as [|n IH].
-    - eexists. split. by rewrite right_id. intros. apply nclose_subseteq.
-    - intros i. destruct (IH (S i)) as [E [IH1 IH2]].
-      eexists (E ∖ (N .@ i))%I. split.
-      + simpl. rewrite IH1 assoc -tl_own_union; last set_solver.
-        f_equiv; last done. f_equiv. rewrite (comm union).
-        apply union_difference_L. apply IH2. lia.
-      + intros. assert (i0 ≠ i)%nat by lia. solve_ndisj.
+    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]".
+      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 %->.
+      iFrame. iExists _, _. by iFrame.
   Qed.
 
-  Program Definition product (tyl : list type) :=
-    {| ty_size := sum_list_with ty_size tyl; ty_dup := forallb ty_dup tyl;
-       ty_own tid vl :=
-         (∃ vll, vl = concat vll ∗ length tyl = length vll ∗
-                 [∗ list] tyvl ∈ combine tyl vll, tyvl.1.(ty_own) tid (tyvl.2))%I;
-       ty_shr κ tid N l :=
-         ([∗ list] i ↦ tyoffs ∈ combine_offs tyl 0,
-           tyoffs.1.(ty_shr) κ tid (N .@ i) (shift_loc l (tyoffs.2)))%I
-    |}.
-  Next Obligation.
-    intros tyl tid vl Hfa.
-    cut (∀ vll, PersistentP ([∗ list] tyvl ∈ combine tyl vll,
-                             ty_own (tyvl.1) tid (tyvl.2))). by apply _.
-    clear vl. induction tyl as [|ty tyl IH]=>[|[|vl vll]]; try by apply _.
-    edestruct andb_prop_elim as [Hduph Hdupq]. by apply Hfa.
-    rewrite /PersistentP /= big_sepL_cons.
-    iIntros "?". by iApply persistentP.
-  Qed.
+  Program Definition product2 (ty1 ty2 : type) :=
+    {| ty_size := ty1.(ty_size) + ty2.(ty_size);
+       ty_dup := ty1.(ty_dup) && ty2.(ty_dup);
+       ty_own tid vl := (∃ vl1 vl2,
+         vl = vl1 ++ vl2 ∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I;
+       ty_shr κ tid E l :=
+         (∃ E1 E2, ■ (E1 ⊥ E2 ∧ E1 ⊆ E ∧ E2 ⊆ E) ∗
+            ty1.(ty_shr) κ tid E1 l ∗
+            ty2.(ty_shr) κ tid E2 (shift_loc l ty1.(ty_size)))%I |}.
+  Next Obligation. intros ty1 ty2 tid vl [Hdup1 Hdup2]%andb_True. apply _. Qed.
   Next Obligation.
-    iIntros (tyl tid vl) "Hown". iDestruct "Hown" as (vll) "(%&%&Hown)".
-    subst. by iApply (list_ty_type_eq with "Hown").
+    iIntros (ty1 ty2 tid vl) "H". iDestruct "H" as (vl1 vl2) "(% & H1 & H2)".
+    subst. rewrite app_length !ty_size_eq.
+    iDestruct "H1" as %->. iDestruct "H2" as %->. done.
   Qed.
   Next Obligation.
-    intros tyl E N κ l tid q ??. rewrite split_prod_mt.
-    change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). generalize O at 3.
-    induction (combine_offs tyl 0) as [|[ty offs] ll IH].
-    - iIntros (?) "_$!>". by rewrite big_sepL_nil.
-    - iIntros (i) "Hown Htoks". rewrite big_sepL_cons.
-      iMod (borrow_split with "Hown") as "[Hownh Hownq]". set_solver.
-      iMod (IH (S i)%nat with "Hownq Htoks") as "[#Hshrq Htoks]".
-      iMod (ty.(ty_share) _ (N .@ (i+0)%nat) with "Hownh Htoks") as "[#Hshrh $]".
-        solve_ndisj. done.
-      iModIntro. rewrite big_sepL_cons. iFrame "#".
-      iApply big_sepL_mono; last done. intros. by rewrite /= Nat.add_succ_r.
+    intros ty1 ty2 E N κ l tid q ??. iIntros "/=H Htok".
+    rewrite split_prod_mt.
+    iMod (borrow_split with "H") as "[H1 H2]". set_solver.
+    iMod (ty1.(ty_share) _ (N .@ 1) with "H1 Htok") as "[? Htok]". solve_ndisj. done.
+    iMod (ty2.(ty_share) _ (N .@ 2) with "H2 Htok") as "[? $]". solve_ndisj. done.
+    iModIntro. iExists (N .@ 1). iExists (N .@ 2). iFrame.
+    iPureIntro. split. solve_ndisj. split; apply nclose_subseteq.
   Qed.
   Next Obligation.
-    iIntros (tyl κ κ' tid N l) "#Hκ #H". iApply big_sepL_impl.
-    iSplit; last done. iIntros "!#*/=_#H'". by iApply (ty_shr_mono with "Hκ").
+    intros ty1 ty2 κ κ' tid E E' l ?. iIntros "/=#H⊑ H".
+    iDestruct "H" as (N1 N2) "(% & H1 & H2)". iExists N1, N2.
+    iSplit. iPureIntro. set_solver.
+    iSplitL "H1"; by iApply (ty_shr_mono with "H⊑").
   Qed.
   Next Obligation.
-    intros tyl κ tid E N l q DUP ?. setoid_rewrite split_prod_mt. generalize 0%nat.
-    change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat).
-    destruct (split_prod_namespace tid N (length tyl)) as [Ef [EQ _]].
-    setoid_rewrite ->EQ. clear EQ. generalize 0%nat.
-    revert q. induction tyl as [|tyh tyq IH].
-    - iIntros (q i offs) "_$!>". iExists 1%Qp. rewrite big_sepL_nil. auto.
-    - simpl in DUP. destruct (andb_prop_elim _ _ DUP) as [DUPh DUPq]. simpl.
-      iIntros (q i offs) "#Hshr([Htokh Htokq]&Htlf&Htlh&Htlq)".
-      rewrite big_sepL_cons Nat.add_0_r.
-      iDestruct "Hshr" as "[Hshrh Hshrq]". setoid_rewrite <-Nat.add_succ_comm.
-      iMod (IH with "Hshrq [$Htokq $Htlf $Htlq]") as (q'q) "[Hownq Hcloseq]".
-      iMod (tyh.(ty_shr_acc) with "Hshrh [$Htokh $Htlh]") as (q'h) "[Hownh Hcloseh]".
-      by pose proof (nclose_subseteq N i); set_solver.
-      destruct (Qp_lower_bound q'h q'q) as (q' & q'0h & q'0q & -> & ->).
-      iExists q'. iModIntro. rewrite big_sepL_cons.
-      rewrite -heap_mapsto_vec_prop_op; last apply ty_size_eq.
-      iDestruct "Hownh" as "[$ Hownh1]".
-      rewrite (big_sepL_proper (λ _ x, _ ↦∗{_}: _)%I); last first.
-      { intros. rewrite -heap_mapsto_vec_prop_op; last apply ty_size_eq.
-        instantiate (1:=λ _ y, _). simpl. reflexivity. }
-      rewrite big_sepL_sepL. iDestruct "Hownq" as "[$ Hownq1]".
-      iIntros "[Hh Hq]". rewrite (lft_own_split κ q).
-      iMod ("Hcloseh" with "[$Hh $Hownh1]") as "[$$]". iApply "Hcloseq". by iFrame.
+    intros ty1 ty2 κ tid E F l q [Hdup1 Hdup2]%andb_True ?.
+    iIntros "H[[Htok1 Htok2] Htl]". iDestruct "H" as (E1 E2) "(% & H1 & H2)".
+    assert (F = E1 ∪ E2 ∪ F∖(E1 ∪ E2)) as ->.
+    { rewrite -union_difference_L; set_solver. }
+    repeat setoid_rewrite tl_own_union; first last.
+    set_solver. set_solver. set_solver. set_solver.
+    iDestruct "Htl" as "[[Htl1 Htl2] $]".
+    iMod (ty1.(ty_shr_acc) with "H1 [$Htok1 $Htl1]") as (q1) "[H1 Hclose1]". set_solver.
+    iMod (ty2.(ty_shr_acc) with "H2 [$Htok2 $Htl2]") as (q2) "[H2 Hclose2]". set_solver.
+    destruct (Qp_lower_bound q1 q2) as (qq & q'1 & q'2 & -> & ->). iExists qq.
+    iDestruct "H1" as (vl1) "[H↦1 H1]". iDestruct "H2" as (vl2) "[H↦2 H2]".
+    rewrite -!heap_mapsto_vec_op_eq !split_prod_mt.
+    iAssert (â–· (length vl1 = ty1.(ty_size)))%I with "[#]" as ">%".
+    { iNext. by iApply ty_size_eq. }
+    iAssert (â–· (length vl2 = ty2.(ty_size)))%I with "[#]" as ">%".
+    { iNext. by iApply ty_size_eq. }
+    iDestruct "H↦1" as "[H↦1 H↦1f]". iDestruct "H↦2" as "[H↦2 H↦2f]".
+    iIntros "!>". iSplitL "H↦1 H1 H↦2 H2".
+    - iNext. iSplitL "H↦1 H1". iExists vl1. by iFrame. iExists vl2. by iFrame.
+    - iIntros "[H1 H2]".
+      iDestruct "H1" as (vl1') "[H↦1 H1]". iDestruct "H2" as (vl2') "[H↦2 H2]".
+      iAssert (â–· (length vl1' = ty1.(ty_size)))%I with "[#]" as ">%".
+      { iNext. by iApply ty_size_eq. }
+      iAssert (â–· (length vl2' = ty2.(ty_size)))%I with "[#]" as ">%".
+      { iNext. by iApply ty_size_eq. }
+      iCombine "H↦1" "H↦1f" as "H↦1". iCombine "H↦2" "H↦2f" as "H↦2".
+      rewrite !heap_mapsto_vec_op; try by congruence.
+      iDestruct "H↦1" as "[_ H↦1]". iDestruct "H↦2" as "[_ H↦2]".
+      iMod ("Hclose1" with "[H1 H↦1]") as "[$$]". by iExists _; iFrame.
+      iMod ("Hclose2" with "[H2 H↦2]") as "[$$]". by iExists _; iFrame. done.
   Qed.
 
+  Definition product (tyl : list type) := fold_right product2 unit tyl.
+
   Lemma split_sum_mt l tid q tyl :
     (l ↦∗{q}: λ vl,
          ∃ (i : nat) vl', vl = #i :: vl' ∗ ty_own (nth i tyl emp) tid vl')%I
@@ -450,13 +397,13 @@ Section types.
     iMod (borrow_fracture with "[-]") as "H"; last by eauto. set_solver. iFrame.
   Qed.
   Next Obligation.
-    intros n tyl Hn κ κ' tid N l. iIntros "#Hord H".
+    intros n tyl Hn κ κ' tid E E' l ?. iIntros "#Hord H".
     iDestruct "H" as (i) "[Hown0 Hown]". iExists i. iSplitL "Hown0".
     by iApply (frac_borrow_shorten with "Hord").
-    by iApply ((nth i tyl emp).(ty_shr_mono) with "Hord").
+    iApply ((nth i tyl emp).(ty_shr_mono) with "Hord"); last done. done.
   Qed.
   Next Obligation.
-    intros n tyl Hn κ tid E N l q Hdup%Is_true_eq_true ?.
+    intros n tyl Hn κ tid E F l q Hdup%Is_true_eq_true ?.
     iIntros "#H[[Htok1 Htok2] Htl]".
     setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 Hshr]".
     iMod (frac_borrow_acc with "[] Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
diff --git a/theories/type_incl.v b/theories/type_incl.v
index 8d78a7fafc902e3b5d791733cae5aa8bbf1fbf4c..7f3c825195560f7ce95a9114b53466ed06af6889 100644
--- a/theories/type_incl.v
+++ b/theories/type_incl.v
@@ -52,7 +52,7 @@ Section ty_incl.
   Proof.
     iIntros (Hincl tid) "H/=". iMod (Hincl with "H") as "[#Howni #Hshri]".
     iModIntro. iSplit; iIntros "!#*H".
-    - iDestruct "H" as (l) "(%&H†&Hmt)". subst. iExists _. iSplit. done.
+    - iDestruct "H" as (l) "(%&Hmt&H†)". subst. iExists _. iSplit. done.
       iDestruct "Hmt" as (vl') "[Hmt Hown]". iNext.
       iDestruct (ty_size_eq with "Hown") as %<-.
       iDestruct ("Howni" $! _ with "Hown") as "Hown".
@@ -81,76 +81,107 @@ Section ty_incl.
       iMod (lft_incl_acc with "Hincl' Htok") as (q'') "[Htok Hclose]". set_solver.
       iMod ("Hupd" with "*Htok") as "Hupd'". iModIntro. iNext.
       iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
-      iApply (ty_shr_mono with "Hincl' H").
+      by iApply (ty_shr_mono with "Hincl' H").
   Qed.
 
   Lemma lft_incl_ty_incl_shared_borrow ty κ1 κ2 :
     ty_incl (κ1 ⊑ κ2) (&shr{κ2}ty) (&shr{κ1}ty).
   Proof.
     iIntros (tid) "#Hincl!>". iSplit; iIntros "!#*H".
-    - iDestruct "H" as (l) "[% Hown]". subst. iExists _. iSplit. done.
-      by iApply (ty.(ty_shr_mono) with "Hincl").
+    - iDestruct "H" as (l) "(% & H)". subst. iExists _.
+      iSplit. done. by iApply (ty.(ty_shr_mono) with "Hincl").
     - iDestruct "H" as (vl) "#[Hfrac Hty]". iSplit; last done.
       iExists vl. iFrame "#". iNext.
-      iDestruct "Hty" as (l0) "[% Hty]". subst. iExists _. iSplit. done.
+      iDestruct "Hty" as (l0) "(% & Hty)". subst. iExists _. iSplit. done.
       by iApply (ty_shr_mono with "Hincl Hty").
   Qed.
 
   (* We have the additional hypothesis that ρ should be duplicable.
      The only way I can see to circumvent this limitation is to deeply
      embed permissions (and their inclusion). Not sure this is worth it. *)
+  Lemma ty_incl_prod2 ρ ty11 ty12 ty21 ty22 :
+    Duplicable ρ → ty_incl ρ ty11 ty12 → ty_incl ρ ty21 ty22 →
+    ty_incl ρ (product2 ty11 ty21) (product2 ty12 ty22).
+  Proof.
+    iIntros (Hρ Hincl1 Hincl2 tid) "#Hρ".
+    iMod (Hincl1 with "Hρ") as "[#Ho1#Hs1]". iMod (Hincl2 with "Hρ") as "[#Ho2#Hs2]".
+    iSplitL; iIntros "!>!#*H/=".
+    - iDestruct "H" as (vl1 vl2) "(% & H1 & H2)". iExists _, _. iSplit. done.
+      iSplitL "H1". iApply ("Ho1" with "H1"). iApply ("Ho2" with "H2").
+    - iDestruct "H" as (E1 E2) "(% & H1 & H2)".
+      iDestruct ("Hs1" with "*H1") as "[H1 EQ]". iDestruct ("Hs2" with "*H2") as "[H2 %]".
+      iDestruct "EQ" as %->. iSplit; last by iPureIntro; f_equal.
+      iExists _, _. by iFrame.
+  Qed.
+
   Lemma ty_incl_prod ρ tyl1 tyl2 :
     Duplicable ρ → Forall2 (ty_incl ρ) tyl1 tyl2 → ty_incl ρ (Π tyl1) (Π tyl2).
+  Proof. intros Hρ HFA. induction HFA. done. by apply ty_incl_prod2. Qed.
+
+  Lemma ty_incl_prod2_assoc1 ρ ty1 ty2 ty3 :
+    ty_incl ρ (product2 ty1 (product2 ty2 ty3)) (product2 (product2 ty1 ty2) ty3).
+  Proof.
+    iIntros (tid) "_!>". iSplit; iIntros "!#/=*H".
+    - iDestruct "H" as (vl1 vl') "(% & Ho1 & H)".
+      iDestruct "H" as (vl2 vl3) "(% & Ho2 & Ho3)". subst.
+      iExists _, _. iSplit. by rewrite assoc. iFrame. iExists _, _. by iFrame.
+    - iDestruct "H" as (E1 E2') "(% & Hs1 & H)".
+      iDestruct "H" as (E2 E3) "(% & Hs2 & Hs3)". rewrite shift_loc_assoc_nat.
+      iSplit; last by rewrite assoc.
+      iExists (E1 ∪ E2), E3. iSplit. by iPureIntro; set_solver. iFrame.
+      iExists E1, E2. iSplit. by iPureIntro; set_solver. by iFrame.
+  Qed.
+
+  Lemma ty_incl_prod2_assoc2 ρ ty1 ty2 ty3 :
+    ty_incl ρ (product2 (product2 ty1 ty2) ty3) (product2 ty1 (product2 ty2 ty3)).
   Proof.
-    intros Hρ HFA. iIntros (tid) "#Hρ". iSplitL "".
-    - assert (Himpl : ρ tid ={⊤}=∗
-         □ (∀ vll, length tyl1 = length vll →
-               ([∗ list] tyvl ∈ combine tyl1 vll, ty_own (tyvl.1) tid (tyvl.2))
-             → ([∗ list] tyvl ∈ combine tyl2 vll, ty_own (tyvl.1) tid (tyvl.2)))).
-      { induction HFA as [|ty1 ty2 tyl1 tyl2 Hincl HFA IH].
-        - iIntros "_!>!#* _ _". by rewrite big_sepL_nil.
-        - iIntros "#Hρ". iMod (IH with "Hρ") as "#Hqimpl".
-          iMod (Hincl with "Hρ") as "[#Hhimpl _]".
-          iIntros "!>!#*%". destruct vll as [|vlh vllq]. done.
-          rewrite !big_sepL_cons.
-          iIntros "[Hh Hq]". iSplitL "Hh". by iApply "Hhimpl".
-          iApply ("Hqimpl" with "[] Hq"). iPureIntro. simpl in *. congruence. }
-      iMod (Himpl with "Hρ") as "#Himpl". iIntros "!>!#*H".
-      iDestruct "H" as (vll) "(%&%&H)". iExists _. iSplit. done. iSplit.
-      by rewrite -(Forall2_length _ _ _ HFA). by iApply ("Himpl" with "[] H").
-    - rewrite /Π /=. iRevert "Hρ". generalize O; intros offs.
-      change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). generalize O; intros i.
-      iInduction HFA as [|ty1 ty2 tyl1 tyl2 Hincl HFA] "IH" forall (i offs).
-      + iIntros "_!>!#*_/=". rewrite big_sepL_nil. eauto.
-      + iIntros "#Hρ". iMod ("IH" $! _ _ with "[]") as "#Hqimpl"; try done.
-        iMod (Hincl with "Hρ") as "[_ #Hhimpl]". iIntros "!>!#*".
-        rewrite !big_sepL_cons. iIntros "[Hh Hq]".
-        setoid_rewrite <-Nat.add_succ_comm.
-        iDestruct ("Hhimpl" $! _ _ _ with "Hh") as "[$ %]".
-        replace ty2.(ty_size) with ty1.(ty_size) by done.
-        iDestruct ("Hqimpl" $! _ _ _ with "Hq") as "[$ %]".
-        iIntros "!%/=". congruence.
-  Qed.
-
-  Lemma ty_incl_prod_cons_l ρ ty tyl :
-    ty_incl ρ (Π(ty :: tyl)) (Π[ty ; Π tyl]).
-  Proof.
-    iIntros (tid) "_!>". iSplit; iIntros "!#/=".
-    - iIntros (vl) "H". iDestruct "H" as ([|vlh vllq]) "(%&%&H)". done. subst.
-      iExists [_;_]. iSplit. by rewrite /= app_nil_r. iSplit. done.
-      rewrite !big_sepL_cons big_sepL_nil right_id. iDestruct "H" as "[$ H]".
-      iExists _. repeat iSplit; try done. iPureIntro. simpl in *; congruence.
-    - iIntros (κ E l) "H". iSplit; last (iPureIntro; lia).
-      rewrite !big_sepL_cons big_sepL_nil right_id. iDestruct "H" as "[$ H]".
-      (* FIXME : namespaces do not match. *)
-      admit.
-  Admitted.
-
-  (* TODO, depends on [ty_incl_prod_cons_l] *)
+    iIntros (tid) "_!>". iSplit; iIntros "!#/=*H".
+    - iDestruct "H" as (vl1 vl') "(% & H & Ho3)".
+      iDestruct "H" as (vl2 vl3) "(% & Ho1 & Ho2)". subst.
+      iExists _, _. iSplit. by rewrite -assoc. iFrame. iExists _, _. by iFrame.
+    - iDestruct "H" as (E1' E3) "(% & H & Hs3)".
+      iDestruct "H" as (E1 E2) "(% & Hs1 & Hs2)". rewrite shift_loc_assoc_nat.
+      iSplit; last by rewrite assoc.
+      iExists E1, (E2 ∪ E3). iSplit. by iPureIntro; set_solver. iFrame.
+      iExists E2, E3. iSplit. by iPureIntro; set_solver. by iFrame.
+  Qed.
+
   Lemma ty_incl_prod_flatten ρ tyl1 tyl2 tyl3 :
     ty_incl ρ (Π(tyl1 ++ Π tyl2 :: tyl3))
               (Π(tyl1 ++ tyl2 ++ tyl3)).
-  Admitted.
+  Proof.
+    apply (ty_incl_weaken _ ⊤). apply perm_incl_top.
+    induction tyl1; last by apply (ty_incl_prod2 _ _ _ _ _ _).
+    induction tyl2 as [|ty tyl2 IH]; simpl.
+    - iIntros (tid) "_". iSplitL; iIntros "/=!>!#*H".
+      + iDestruct "H" as (vl1 vl2) "(% & % & Ho)". subst. done.
+      + iDestruct "H" as (E1 E2) "(% & H1 & Ho)". iSplit; last done.
+        rewrite shift_loc_0. iApply (ty_shr_mono with "[] Ho"). set_solver.
+        iApply lft_incl_refl.
+    - etransitivity. apply ty_incl_prod2_assoc2.
+      eapply (ty_incl_prod2 _ _ _ _ _ _). done. apply IH.
+  Qed.
+
+  Lemma ty_incl_prod_unflatten ρ tyl1 tyl2 tyl3 :
+    ty_incl ρ (Π(tyl1 ++ tyl2 ++ tyl3))
+              (Π(tyl1 ++ Π tyl2 :: tyl3)).
+  Proof.
+    apply (ty_incl_weaken _ ⊤). apply perm_incl_top.
+    induction tyl1; last by apply (ty_incl_prod2 _ _ _ _ _ _).
+    induction tyl2 as [|ty tyl2 IH]; simpl.
+    - iIntros (tid) "_".
+      iMod (borrow_create with "[]") as "[Hbor _]".
+      done. instantiate (1:=True%I). by auto. instantiate (1:=static).
+      iMod (borrow_fracture (λ _, True%I) with "Hbor") as "#Hbor". done.
+      iSplitL; iIntros "/=!>!#*H".
+      + iExists [], vl. iFrame. auto.
+      + iSplit; last done. iExists ∅, E. iSplit. iPureIntro; set_solver.
+        rewrite shift_loc_0. iFrame. iExists []. iSplit; last auto.
+        setoid_rewrite heap_mapsto_vec_nil.
+        iApply (frac_borrow_shorten with "[] Hbor"). iApply lft_incl_static.
+    - etransitivity; last apply ty_incl_prod2_assoc1.
+      eapply (ty_incl_prod2 _ _ _ _ _ _). done. apply IH.
+  Qed.
 
   Lemma ty_incl_sum ρ n tyl1 tyl2 (_ : LstTySize n tyl1) (_ : LstTySize n tyl2) :
     Duplicable ρ → Forall2 (ty_incl ρ) tyl1 tyl2 →
diff --git a/theories/typing.v b/theories/typing.v
index a334f3ad5e228414fa86f2278f618a9d3e81f5ba..f797361a95aa08b5a592289b2059dee17454f6ba 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -150,17 +150,14 @@ Section typing.
     0 < n → typed_step_ty ρ (Alloc #n) (own 1 (Π(replicate n uninit))).
   Proof.
     iIntros (Hn tid) "!#(#HEAP&_&$)". wp_alloc l vl as "H↦" "H†". iIntros "!>".
-    iExists _. iSplit. done. iNext. rewrite Nat2Z.id. iSplitL "H†".
-    - assert (ty_size (Π (replicate n uninit)) = n) as ->; last done.
-      clear. simpl. induction n. done. rewrite /= IHn //.
+    iExists _. iSplit. done. iNext. rewrite Nat2Z.id. iSplitR "H†".
     - iExists vl. iFrame.
       match goal with H : Z.of_nat n = Z.of_nat (length vl) |- _ => rename H into Hlen end.
       clear Hn. apply (inj Z.of_nat) in Hlen. subst.
-      iInduction vl as [|v vl] "IH".
-      + iExists []. rewrite big_sepL_nil. auto.
-      + iDestruct "IH" as (vll) "(% & % & ?)". subst. iExists ([_]::_). iSplit. done.
-        iSplit. iIntros "/=!%"; congruence.
-        rewrite /= big_sepL_cons. by iSplit.
+      iInduction vl as [|v vl] "IH". done.
+      iExists [v], vl. iSplit. done. by iSplit.
+    - assert (ty_size (Π (replicate n uninit)) = n) as ->; last done.
+      clear. simpl. induction n. done. rewrite /= IHn //.
   Qed.
 
   Lemma typed_free ty (ν : expr):
@@ -169,7 +166,7 @@ Section typing.
     iIntros (tid) "!#(#HEAP&H◁&$)". wp_bind ν.
     iApply (has_type_wp with "[$H◁]"). iIntros (v) "[_ H◁]!>".
     rewrite has_type_value.
-    iDestruct "H◁" as (l) "(Hv & >H† & H↦∗:)". iDestruct "Hv" as %[=->].
+    iDestruct "H◁" as (l) "(Hv & H↦∗: & >H†)". iDestruct "Hv" as %[=->].
     iDestruct "H↦∗:" as (vl) "[>H↦ Hown]".
     rewrite ty_size_eq. iDestruct "Hown" as ">%". wp_free; eauto.
   Qed.
@@ -188,7 +185,7 @@ Section typing.
   Proof.
     iIntros (? ν tid Φ E ?) "(H◁ & Htl & HΦ)". iApply (has_type_wp with "[- $H◁]").
     iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
-    rewrite has_type_value. iDestruct "H◁" as (l) "[Heq [>H† H↦]]".
+    rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦ & >H†)".
     iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
       by rewrite ty.(ty_size_eq).
@@ -202,21 +199,17 @@ Section typing.
   Proof.
     iIntros (ν tid Φ E ?) "(H◁ & Htl & HΦ)". iApply (has_type_wp with "[- $H◁]").
     iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
-    rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & >H† & H↦)".
+    rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦ & >H†)".
     iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">Hlen".
       by rewrite ty.(ty_size_eq). iDestruct "Hlen" as %Hlen.
     iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦!>".
-    rewrite /has_type Hνv. iExists _. iSplit. done. iSplitL "H†".
+    rewrite /has_type Hνv. iExists _. iSplit. done. iSplitR "H†".
+    - rewrite -Hlen. iExists vl. iIntros "{$H↦}!>". clear.
+      iInduction vl as [|v vl] "IH". done.
+      iExists [v], vl. iSplit. done. by iSplit.
     - assert (ty_size (Π (replicate (ty_size ty) uninit)) = ty_size ty) as ->; last by auto.
       clear. induction ty.(ty_size). done. simpl in *. congruence.
-    - rewrite -Hlen. iExists vl. iIntros "{$H↦}!>". clear.
-      iInduction vl as [|v vl] "IH".
-      + iExists []. rewrite big_sepL_nil. auto.
-      + iDestruct "IH" as (vll) "(% & % & IH)". iExists ([v]::vll). iSplit; last iSplit.
-        * iIntros "!%/=". congruence.
-        * iIntros "!%/=". congruence.
-        * rewrite big_sepL_cons. iFrame "#". done.
   Qed.
 
   Lemma consumes_copy_uniq_borrow ty κ κ' q:
@@ -262,8 +255,8 @@ Section typing.
     typed_step (ρ1 ν) (!ν) (λ v, v ◁ ty ∗ ρ2 ν)%P.
   Proof.
     iIntros (Hsz Hconsumes tid) "!#[#HEAP[??]]". wp_bind ν.
-    iApply Hconsumes. done. iFrame. iIntros (l vl q) "(%&%&H↦&Hupd)".
-    iMod "Hupd". rewrite ->Hsz in *. destruct vl as [|v [|]]; try done.
+    iApply Hconsumes. done. iFrame. iIntros (l vl q) "(%&%&H↦&>Hupd)".
+    rewrite ->Hsz in *. destruct vl as [|v [|]]; try done.
     rewrite heap_mapsto_vec_singleton. wp_read. rewrite /sep has_type_value.
     iMod "Hupd" as "[$ Hclose]". by iApply "Hclose".
   Qed.
@@ -278,9 +271,9 @@ Section typing.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
     iMod (borrow_acc_strong with "H↦ Htok") as "[H↦ Hclose']". done.
-    iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct "Hown" as (l') "(>% & H† & Hown)".
+    iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct "Hown" as (l') "(>% & Hown & H†)".
     subst. rewrite heap_mapsto_vec_singleton. wp_read.
-    iMod ("Hclose'" with "*[H↦ H† Hown]") as "[Hbor Htok]"; last first.
+    iMod ("Hclose'" with "*[H↦ Hown H†]") as "[Hbor Htok]"; last first.
     - iMod (borrow_split with "Hbor") as "[_ Hbor]". done.
       iMod (borrow_split with "Hbor") as "[_ Hbor]". done.
       iMod ("Hclose" with "Htok") as "$". iFrame "#". iExists _. eauto.
@@ -360,7 +353,7 @@ Section typing.
       iMod ("Hclose''" with "Htok") as "Htok".
       iMod ("Hclose'" with "[$H↦]") as "Htok'".
       iMod ("Hclose" with "[$Htok $Htok']") as "$". iFrame "#". iExists _.
-      iSplitL. done. iApply (ty_shr_mono with "H⊑3 Hshr").
+      iSplitL. done. by iApply (ty_shr_mono with "H⊑3 Hshr").
   Qed.
 
   Definition update (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
@@ -378,7 +371,7 @@ Section typing.
   Proof.
     iIntros (Hsz ν tid Φ E ?) "[H◁ HΦ]". iApply (has_type_wp with "[- $H◁]").
     iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
-    rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & >H† & H↦)".
+    rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦ & >H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
     rewrite ty2.(ty_size_eq) -Hsz. iDestruct "Hown" as ">%". iApply "HΦ". iFrame "∗%".
     iIntros (vl') "[H↦ Hown']!>". rewrite /has_type Hνv.