diff --git a/theories/type.v b/theories/type.v
index 46231d466240721d2a80b4a0690155e3c90bec5e..b5d228ac3f12c37bfaad5202c9f5af8de07627bc 100644
--- a/theories/type.v
+++ b/theories/type.v
@@ -66,7 +66,7 @@ Program Coercion ty_of_st (st : simple_type) : type :=
      ty_own := st.(st_own);
 
      (* [st.(st_own) tid vl] needs to be outside of the fractured
-        borrow, otherwise I do not knwo how to prove the shr part of
+        borrow, otherwise I do not know how to prove the shr part of
         [lft_incl_ty_incl_shared_borrow]. *)
      ty_shr := λ κ tid _ l,
                (∃ vl, (&frac{κ} λ q, l ↦∗{q} vl) ∗ ▷ st.(st_own) tid vl)%I
@@ -482,8 +482,8 @@ Section types.
       by iApply "Hclose'".
   Qed.
 
-  Program Definition uninit (n : nat) : type :=
-    {| st_size := n; st_own tid vl := (length vl = n)%I |}.
+  Program Definition uninit : type :=
+    {| st_size := 1; st_own tid vl := (length vl = 1%nat)%I |}.
   Next Obligation. done. Qed.
 
   Program Definition cont {n : nat} (ρ : vec val n → @perm Σ) :=
diff --git a/theories/type_incl.v b/theories/type_incl.v
index 2c8a0c1cbc1574170f0897302dfdb18d97f09ba1..8d78a7fafc902e3b5d791733cae5aa8bbf1fbf4c 100644
--- a/theories/type_incl.v
+++ b/theories/type_incl.v
@@ -180,32 +180,6 @@ Section ty_incl.
       iDestruct "H" as (i) "[??]". iExists _. iSplit. done. by iApply "Hincl".
   Qed.
 
-  Lemma ty_incl_uninit_split ρ n1 n2 :
-    ty_incl ρ (uninit (n1+n2)) (Π[uninit n1; uninit n2]).
-  Proof.
-    iIntros (tid) "_!>". iSplit; iIntros "!#*H".
-    - iDestruct "H" as %Hlen. iExists [take n1 vl; drop n1 vl].
-      repeat iSplit. by rewrite /= app_nil_r take_drop. done.
-      rewrite big_sepL_cons big_sepL_singleton. iSplit; iPureIntro.
-      apply take_length_le. lia. rewrite drop_length. lia.
-    - iSplit; last (iPureIntro; simpl; lia). iDestruct "H" as (vl) "[#Hf #Hlen]".
-      rewrite /= big_sepL_cons big_sepL_singleton. iSplit.
-      + iExists (take n1 vl). iSplit.
-        (* FIXME : cannot split the fractured borrow. *)
-        admit.
-        iNext. iDestruct "Hlen" as %Hlen. rewrite /= take_length_le //. lia.
-      + iExists (drop n1 vl). iSplit.
-        (* FIXME : cannot split the fractured borrow. *)
-        admit.
-        iNext. iDestruct "Hlen" as %Hlen. rewrite /= drop_length. iPureIntro. lia.
-  Admitted.
-
-  Lemma ty_incl_uninit_combine ρ n1 n2 :
-    ty_incl ρ (Π[uninit n1; uninit n2]) (uninit (n1+n2)).
-  Proof.
-  (* FIXME : idem : cannot combine the fractured borrow. *)
-  Admitted.
-
   Lemma ty_incl_cont {n} ρ ρ1 ρ2 :
     Duplicable ρ → (∀ vl : vec val n, ρ ∗ ρ2 vl ⇒ ρ1 vl) →
     ty_incl ρ (cont ρ1) (cont ρ2).
diff --git a/theories/typing.v b/theories/typing.v
index 9e8d0a004d1a6ae86c864405efed48f8462e9a9a..a334f3ad5e228414fa86f2278f618a9d3e81f5ba 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -1,4 +1,5 @@
 From iris.program_logic Require Import hoare.
+From iris.base_logic Require Import big_op.
 From lrust Require Export type perm notation memcpy.
 From lrust Require Import perm_incl proofmode.
 
@@ -146,11 +147,20 @@ Section typing.
   Qed.
 
   Lemma typed_alloc ρ (n : nat):
-    0 < n → typed_step_ty ρ (Alloc #n) (own 1 (uninit n)).
+    0 < n → typed_step_ty ρ (Alloc #n) (own 1 (Π(replicate n uninit))).
   Proof.
-    iIntros (? tid) "!#(#HEAP&_&$)". wp_alloc l vl as "H↦" "H†". iIntros "!>".
-    iExists _. iSplit. done. iNext. rewrite Nat2Z.id. iFrame.
-    iExists _. iFrame. iPureIntro. by apply (inj Z.of_nat).
+    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 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.
   Qed.
 
   Lemma typed_free ty (ν : expr):
@@ -187,16 +197,26 @@ Section typing.
   Qed.
 
   Lemma consumes_move ty q:
-    consumes ty (λ ν, ν ◁ own q ty)%P (λ ν, ν ◁ own q (uninit ty.(ty_size)))%P.
+    consumes ty (λ ν, ν ◁ own q ty)%P
+             (λ ν, ν ◁ own q (Π(replicate ty.(ty_size) uninit)))%P.
   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↦)".
     iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
-    iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
-      by rewrite ty.(ty_size_eq).
+    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. iFrame. iExists vl. eauto.
+    rewrite /has_type Hνv. iExists _. iSplit. done. iSplitL "H†".
+    - 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: