diff --git a/CHANGELOG.md b/CHANGELOG.md
index bde91d87d7504c3c76d81607f6e93db8a1c64f97..01c9684d1c2f5d4402fa2843fad9be4f157eff24 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -68,6 +68,11 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * Add new introduction pattern `-# pat` that moves a hypothesis from the
   intuitionistic context to the spatial context.
 
+**Changes in heap_lang:**
+
+* Added a fraction to the heap_lang `array` assertion.
+
+
 ## Iris 3.2.0 (released 2019-08-29)
 
 The highlight of this release is the completely re-engineered interactive proof
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 5c56f67f3c583257cc461fa005d42e69d08b504d..075424338a0ad49e124b52b9c1d02a07def0b5d0 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -86,16 +86,20 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   --------------------------------------âˆ—
   WP "x" {{ _, True }}
   
-The command has indeed failed with message:
-In nested Ltac calls to "iIntros (constr)", "iIntros_go",
-"iDestructHyp (constr) as (constr)",
-"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
-"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
-"iAndDestruct (constr) as (constr) (constr)", last call failed.
-Tactic failure: iAndDestruct: cannot destruct (l â†¦âˆ— (vs1 ++ vs2))%I.
-The command has indeed failed with message:
-Ltac call to "iSplitL (constr)" failed.
-Tactic failure: iSplitL: (l â†¦âˆ— (vs1 ++ vs2))%I not a separating conjunction.
+"test_array_fraction_destruct"
+     : string
+1 subgoal
+  
+  Î£ : gFunctors
+  heapG0 : heapG Î£
+  l : loc
+  vs : list val
+  ============================
+  "Hl1" : l â†¦âˆ—{1 / 2} vs
+  "Hl2" : l â†¦âˆ—{1 / 2} vs
+  --------------------------------------âˆ—
+  l â†¦âˆ—{1 / 2} vs âˆ— l â†¦âˆ—{1 / 2} vs
+  
 1 subgoal
   
   Î£ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index f971580a987be3143201b9befedb5b1866684a38..047fb65c2694feea51bdfd484ac546a27feb164d 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -159,19 +159,38 @@ Section tests.
     {{{ l â†¦âˆ— [ #0;#1;#2 ] }}} !(#l +â‚— #1) {{{ RET #1; True }}}.
   Proof.
     iIntros (Î¦) "Hl HÎ¦". wp_op.
-    wp_apply (wp_load_offset _ _ _ 1 with "Hl"); first done.
+    wp_apply (wp_load_offset _ _ _ _ 1 with "Hl"); first done.
     iIntros "Hl". by iApply "HÎ¦".
   Qed.
 
+  Check "test_array_fraction_destruct".
+  Lemma test_array_fraction_destruct l vs :
+    l â†¦âˆ— vs -âˆ— l â†¦âˆ—{1/2} vs âˆ— l â†¦âˆ—{1/2} vs.
+  Proof.
+    iIntros "[Hl1 Hl2]". Show.
+    by iFrame.
+  Qed.
+
+  Lemma test_array_fraction_combine l vs :
+    l â†¦âˆ—{1/2} vs -âˆ— lâ†¦âˆ—{1/2} vs -âˆ— l â†¦âˆ— vs.
+  Proof.
+    iIntros "Hl1 Hl2".
+    iSplitL "Hl1"; by iFrame.
+  Qed.
+
   Lemma test_array_app l vs1 vs2 :
     l â†¦âˆ— (vs1 ++ vs2) -âˆ— l â†¦âˆ— (vs1 ++ vs2).
   Proof.
-    Fail iIntros "[H1 H2]". (* this should, one day, split at the fraction. *)
     iIntros "H". iDestruct (array_app with "H") as "[H1 H2]".
-    Fail iSplitL "H1".
     iApply array_app. iSplitL "H1"; done.
   Qed.
 
+  Lemma test_array_app_split l vs1 vs2 :
+    l â†¦âˆ— (vs1 ++ vs2) -âˆ— l â†¦âˆ—{1/2} (vs1 ++ vs2).
+  Proof.
+    iIntros "[$ _]". (* splits the fraction, not the app *)
+  Qed.
+
 End tests.
 
 Section printing_tests.
diff --git a/theories/heap_lang/array.v b/theories/heap_lang/array.v
index 7e889c9e45be576b92ecfc51cea1a9dac90a106d..43c64c41f916da7da52dca6e623a4895cbb4d4ca 100644
--- a/theories/heap_lang/array.v
+++ b/theories/heap_lang/array.v
@@ -1,4 +1,5 @@
 From stdpp Require Import fin_maps.
+From iris.bi Require Import lib.fractional.
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lifting.
@@ -7,16 +8,18 @@ Set Default Proof Using "Type".
 
 (** This file defines the [array] connective, a version of [mapsto] that works
 with lists of values. It also contains array versions of the basic heap
-operations of HeapLand. *)
+operations of HeapLang. *)
 
-Definition array `{!heapG Î£} (l : loc) (vs : list val) : iProp Î£ :=
-  ([âˆ— list] i â†¦ v âˆˆ vs, (l +â‚— i) â†¦ v)%I.
-Notation "l â†¦âˆ— vs" := (array l vs)
+Definition array `{!heapG Î£} (l : loc) (q : Qp) (vs : list val) : iProp Î£ :=
+  ([âˆ— list] i â†¦ v âˆˆ vs, (l +â‚— i) â†¦{q} v)%I.
+Notation "l â†¦âˆ—{ q } vs" := (array l q vs)
+  (at level 20, q at level 50, format "l  â†¦âˆ—{ q }  vs") : bi_scope.
+Notation "l â†¦âˆ— vs" := (array l 1 vs)
   (at level 20, format "l  â†¦âˆ—  vs") : bi_scope.
 
-(** We have no [FromSep] or [IntoSep] instances to remain forwards compatible
-with a fractional array assertion, that will split the fraction, not the
-list. *)
+(** We have [FromSep] and [IntoSep] instances to split the fraction (via the
+[AsFractional] instance below), but not for splitting the list, as that would
+lead to overlapping instances. *)
 
 Section lifting.
 Context `{!heapG Î£}.
@@ -25,26 +28,32 @@ Implicit Types Î¦ : val â†’ iProp Î£.
 Implicit Types Ïƒ : state.
 Implicit Types v : val.
 Implicit Types vs : list val.
+Implicit Types q : Qp.
 Implicit Types l : loc.
 Implicit Types sz off : nat.
 
-Global Instance array_timeless l vs : Timeless (array l vs) := _.
+Global Instance array_timeless l q vs : Timeless (array l q vs) := _.
 
-Lemma array_nil l : l â†¦âˆ— [] âŠ£âŠ¢ emp.
+Global Instance array_fractional l vs : Fractional (Î» q, l â†¦âˆ—{q} vs)%I := _.
+Global Instance array_as_fractional l q vs :
+  AsFractional (l â†¦âˆ—{q} vs) (Î» q, l â†¦âˆ—{q} vs)%I q.
+Proof. split; done || apply _. Qed.
+
+Lemma array_nil l q : l â†¦âˆ—{q} [] âŠ£âŠ¢ emp.
 Proof. by rewrite /array. Qed.
 
-Lemma array_singleton l v : l â†¦âˆ— [v] âŠ£âŠ¢ l â†¦ v.
+Lemma array_singleton l q v : l â†¦âˆ—{q} [v] âŠ£âŠ¢ l â†¦{q} v.
 Proof. by rewrite /array /= right_id loc_add_0. Qed.
 
-Lemma array_app l vs ws :
-  l â†¦âˆ— (vs ++ ws) âŠ£âŠ¢ l â†¦âˆ— vs âˆ— (l +â‚— length vs) â†¦âˆ— ws.
+Lemma array_app l q vs ws :
+  l â†¦âˆ—{q} (vs ++ ws) âŠ£âŠ¢ l â†¦âˆ—{q} vs âˆ— (l +â‚— length vs) â†¦âˆ—{q} ws.
 Proof.
   rewrite /array big_sepL_app.
   setoid_rewrite Nat2Z.inj_add.
   by setoid_rewrite loc_add_assoc.
 Qed.
 
-Lemma array_cons l v vs : l â†¦âˆ— (v :: vs) âŠ£âŠ¢ l â†¦ v âˆ— (l +â‚— 1) â†¦âˆ— vs.
+Lemma array_cons l q v vs : l â†¦âˆ—{q} (v :: vs) âŠ£âŠ¢ l â†¦{q} v âˆ— (l +â‚— 1) â†¦âˆ—{q} vs.
 Proof.
   rewrite /array big_sepL_cons loc_add_0.
   setoid_rewrite loc_add_assoc.
@@ -52,12 +61,12 @@ Proof.
   by setoid_rewrite Z.add_1_l.
 Qed.
 
-Lemma update_array l vs off v :
+Lemma update_array l q vs off v :
   vs !! off = Some v â†’
-  (l â†¦âˆ— vs -âˆ— ((l +â‚— off) â†¦ v âˆ— âˆ€ v', (l +â‚— off) â†¦ v' -âˆ— l â†¦âˆ— <[off:=v']>vs))%I.
+  l â†¦âˆ—{q} vs -âˆ— ((l +â‚— off) â†¦{q} v âˆ— âˆ€ v', (l +â‚— off) â†¦{q} v' -âˆ— l â†¦âˆ—{q} <[off:=v']>vs).
 Proof.
   iIntros (Hlookup) "Hl".
-  rewrite -[X in (l â†¦âˆ— X)%I](take_drop_middle _ off v); last done.
+  rewrite -[X in (l â†¦âˆ—{_} X)%I](take_drop_middle _ off v); last done.
   iDestruct (array_app with "Hl") as "[Hl1 Hl]".
   iDestruct (array_cons with "Hl") as "[Hl2 Hl3]".
   assert (off < length vs)%nat as H by (apply lookup_lt_is_Some; by eexists).
@@ -65,16 +74,16 @@ Proof.
   iIntros (w) "Hl2".
   clear Hlookup. assert (<[off:=w]> vs !! off = Some w) as Hlookup.
   { apply list_lookup_insert. lia. }
-  rewrite -[in (l â†¦âˆ— <[off:=w]> vs)%I](take_drop_middle (<[off:=w]> vs) off w Hlookup).
+  rewrite -[in (l â†¦âˆ—{_} <[off:=w]> vs)%I](take_drop_middle (<[off:=w]> vs) off w Hlookup).
   iApply array_app. rewrite take_insert; last by lia. iFrame.
   iApply array_cons. rewrite take_length min_l; last by lia. iFrame.
   rewrite drop_insert; last by lia. done.
 Qed.
 
 (** Allocation *)
-Lemma mapsto_seq_array l v n :
-  ([âˆ— list] i âˆˆ seq 0 n, (l +â‚— (i : nat)) â†¦ v) -âˆ—
-  l â†¦âˆ— replicate n v.
+Lemma mapsto_seq_array l q v n :
+  ([âˆ— list] i âˆˆ seq 0 n, (l +â‚— (i : nat)) â†¦{q} v) -âˆ—
+  l â†¦âˆ—{q} replicate n v.
 Proof.
   rewrite /array. iInduction n as [|n'] "IH" forall (l); simpl.
   { done. }
@@ -129,33 +138,33 @@ Qed.
 
 (** Access to array elements *)
 
-Lemma wp_load_offset s E l off vs v :
+Lemma wp_load_offset s E l q off vs v :
   vs !! off = Some v â†’
-  {{{ â–· l â†¦âˆ— vs }}} ! #(l +â‚— off) @ s; E {{{ RET v; l â†¦âˆ— vs }}}.
+  {{{ â–· l â†¦âˆ—{q} vs }}} ! #(l +â‚— off) @ s; E {{{ RET v; l â†¦âˆ—{q} vs }}}.
 Proof.
   iIntros (Hlookup Î¦) "Hl HÎ¦".
-  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
   iApply (wp_load with "Hl1"). iIntros "!> Hl1". iApply "HÎ¦".
   iDestruct ("Hl2" $! v) as "Hl2". rewrite list_insert_id; last done.
   iApply "Hl2". iApply "Hl1".
 Qed.
-Lemma twp_load_offset s E l off vs v :
+Lemma twp_load_offset s E l q off vs v :
   vs !! off = Some v â†’
-  [[{ l â†¦âˆ— vs }]] ! #(l +â‚— off) @ s; E [[{ RET v; l â†¦âˆ— vs }]].
+  [[{ l â†¦âˆ—{q} vs }]] ! #(l +â‚— off) @ s; E [[{ RET v; l â†¦âˆ—{q} vs }]].
 Proof.
   iIntros (Hlookup Î¦) "Hl HÎ¦".
-  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
   iApply (twp_load with "Hl1"). iIntros "Hl1". iApply "HÎ¦".
   iDestruct ("Hl2" $! v) as "Hl2". rewrite list_insert_id; last done.
   iApply "Hl2". iApply "Hl1".
 Qed.
 
 
-Lemma wp_load_offset_vec s E l sz (off : fin sz) (vs : vec val sz) :
-  {{{ â–· l â†¦âˆ— vs }}} ! #(l +â‚— off) @ s; E {{{ RET vs !!! off; l â†¦âˆ— vs }}}.
+Lemma wp_load_offset_vec s E l q sz (off : fin sz) (vs : vec val sz) :
+  {{{ â–· l â†¦âˆ—{q} vs }}} ! #(l +â‚— off) @ s; E {{{ RET vs !!! off; l â†¦âˆ—{q} vs }}}.
 Proof. apply wp_load_offset. by apply vlookup_lookup. Qed.
-Lemma twp_load_offset_vec s E l sz (off : fin sz) (vs : vec val sz) :
-  [[{ l â†¦âˆ— vs }]] ! #(l +â‚— off) @ s; E [[{ RET vs !!! off; l â†¦âˆ— vs }]].
+Lemma twp_load_offset_vec s E l q sz (off : fin sz) (vs : vec val sz) :
+  [[{ l â†¦âˆ—{q} vs }]] ! #(l +â‚— off) @ s; E [[{ RET vs !!! off; l â†¦âˆ—{q} vs }]].
 Proof. apply twp_load_offset. by apply vlookup_lookup. Qed.
 
 
@@ -164,7 +173,7 @@ Lemma wp_store_offset s E l off vs v :
   {{{ â–· l â†¦âˆ— vs }}} #(l +â‚— off) <- v @ s; E {{{ RET #(); l â†¦âˆ— <[off:=v]> vs }}}.
 Proof.
   iIntros ([w Hlookup] Î¦) ">Hl HÎ¦".
-  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
   iApply (wp_store with "Hl1"). iNext. iIntros "Hl1".
   iApply "HÎ¦". iApply "Hl2". iApply "Hl1".
 Qed.
@@ -173,7 +182,7 @@ Lemma twp_store_offset s E l off vs v :
   [[{ l â†¦âˆ— vs }]] #(l +â‚— off) <- v @ s; E [[{ RET #(); l â†¦âˆ— <[off:=v]> vs }]].
 Proof.
   iIntros ([w Hlookup] Î¦) "Hl HÎ¦".
-  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
   iApply (twp_store with "Hl1"). iIntros "Hl1".
   iApply "HÎ¦". iApply "Hl2". iApply "Hl1".
 Qed.
@@ -200,7 +209,7 @@ Lemma wp_cmpxchg_suc_offset s E l off vs v' v1 v2 :
   {{{ RET (v', #true); l â†¦âˆ— <[off:=v2]> vs }}}.
 Proof.
   iIntros (Hlookup ?? Î¦) "Hl HÎ¦".
-  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
   iApply (wp_cmpxchg_suc with "Hl1"); [done..|].
   iNext. iIntros "Hl1". iApply "HÎ¦". iApply "Hl2". iApply "Hl1".
 Qed.
@@ -213,7 +222,7 @@ Lemma twp_cmpxchg_suc_offset s E l off vs v' v1 v2 :
   [[{ RET (v', #true); l â†¦âˆ— <[off:=v2]> vs }]].
 Proof.
   iIntros (Hlookup ?? Î¦) "Hl HÎ¦".
-  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
   iApply (twp_cmpxchg_suc with "Hl1"); [done..|].
   iIntros "Hl1". iApply "HÎ¦". iApply "Hl2". iApply "Hl1".
 Qed.
@@ -239,50 +248,50 @@ Proof.
   by apply vlookup_lookup.
 Qed.
 
-Lemma wp_cmpxchg_fail_offset s E l off vs v0 v1 v2 :
+Lemma wp_cmpxchg_fail_offset s E l q off vs v0 v1 v2 :
   vs !! off = Some v0 â†’
   v0 â‰  v1 â†’
   vals_compare_safe v0 v1 â†’
-  {{{ â–· l â†¦âˆ— vs }}}
+  {{{ â–· l â†¦âˆ—{q} vs }}}
     CmpXchg #(l +â‚— off) v1 v2 @ s; E
-  {{{ RET (v0, #false); l â†¦âˆ— vs }}}.
+  {{{ RET (v0, #false); l â†¦âˆ—{q} vs }}}.
 Proof.
   iIntros (Hlookup HNEq Hcmp Î¦) ">Hl HÎ¦".
-  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
   iApply (wp_cmpxchg_fail with "Hl1"); first done.
   { destruct Hcmp; by [ left | right ]. }
   iIntros "!> Hl1". iApply "HÎ¦". iDestruct ("Hl2" $! v0) as "Hl2".
   rewrite list_insert_id; last done. iApply "Hl2". iApply "Hl1".
 Qed.
-Lemma twp_cmpxchg_fail_offset s E l off vs v0 v1 v2 :
+Lemma twp_cmpxchg_fail_offset s E l q off vs v0 v1 v2 :
   vs !! off = Some v0 â†’
   v0 â‰  v1 â†’
   vals_compare_safe v0 v1 â†’
-  [[{ l â†¦âˆ— vs }]]
+  [[{ l â†¦âˆ—{q} vs }]]
     CmpXchg #(l +â‚— off) v1 v2 @ s; E
-  [[{ RET (v0, #false); l â†¦âˆ— vs }]].
+  [[{ RET (v0, #false); l â†¦âˆ—{q} vs }]].
 Proof.
   iIntros (Hlookup HNEq Hcmp Î¦) "Hl HÎ¦".
-  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
   iApply (twp_cmpxchg_fail with "Hl1"); first done.
   { destruct Hcmp; by [ left | right ]. }
   iIntros "Hl1". iApply "HÎ¦". iDestruct ("Hl2" $! v0) as "Hl2".
   rewrite list_insert_id; last done. iApply "Hl2". iApply "Hl1".
 Qed.
 
-Lemma wp_cmpxchg_fail_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
+Lemma wp_cmpxchg_fail_offset_vec s E l q sz (off : fin sz) (vs : vec val sz) v1 v2 :
   vs !!! off â‰  v1 â†’
   vals_compare_safe (vs !!! off) v1 â†’
-  {{{ â–· l â†¦âˆ— vs }}}
+  {{{ â–· l â†¦âˆ—{q} vs }}}
     CmpXchg #(l +â‚— off) v1 v2 @ s; E
-  {{{ RET (vs !!! off, #false); l â†¦âˆ— vs }}}.
+  {{{ RET (vs !!! off, #false); l â†¦âˆ—{q} vs }}}.
 Proof. intros. eapply wp_cmpxchg_fail_offset=> //. by apply vlookup_lookup. Qed.
-Lemma twp_cmpxchg_fail_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
+Lemma twp_cmpxchg_fail_offset_vec s E l q sz (off : fin sz) (vs : vec val sz) v1 v2 :
   vs !!! off â‰  v1 â†’
   vals_compare_safe (vs !!! off) v1 â†’
-  [[{ l â†¦âˆ— vs }]]
+  [[{ l â†¦âˆ—{q} vs }]]
     CmpXchg #(l +â‚— off) v1 v2 @ s; E
-  [[{ RET (vs !!! off, #false); l â†¦âˆ— vs }]].
+  [[{ RET (vs !!! off, #false); l â†¦âˆ—{q} vs }]].
 Proof. intros. eapply twp_cmpxchg_fail_offset=> //. by apply vlookup_lookup. Qed.
 
 Lemma wp_faa_offset s E l off vs (i1 i2 : Z) :
@@ -291,7 +300,7 @@ Lemma wp_faa_offset s E l off vs (i1 i2 : Z) :
   {{{ RET LitV (LitInt i1); l â†¦âˆ— <[off:=#(i1 + i2)]> vs }}}.
 Proof.
   iIntros (Hlookup Î¦) "Hl HÎ¦".
-  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
   iApply (wp_faa with "Hl1").
   iNext. iIntros "Hl1". iApply "HÎ¦". iApply "Hl2". iApply "Hl1".
 Qed.
@@ -301,7 +310,7 @@ Lemma twp_faa_offset s E l off vs (i1 i2 : Z) :
   [[{ RET LitV (LitInt i1); l â†¦âˆ— <[off:=#(i1 + i2)]> vs }]].
 Proof.
   iIntros (Hlookup Î¦) "Hl HÎ¦".
-  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
   iApply (twp_faa with "Hl1").
   iIntros "Hl1". iApply "HÎ¦". iApply "Hl2". iApply "Hl1".
 Qed.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index d1632a886c41ec2fb8b5787ec375480c84a1eda0..9f10d6010e614e7d6f3cad50b9ee09262a581a38 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -187,7 +187,7 @@ Lemma tac_wp_allocN Î” Î”' s E j K v n Î¦ :
   0 < n â†’
   MaybeIntoLaterNEnvs 1 Î” Î”' â†’
   (âˆ€ l, âˆƒ Î”'',
-    envs_app false (Esnoc Enil j (array l (replicate (Z.to_nat n) v))) Î”' = Some Î”'' âˆ§
+    envs_app false (Esnoc Enil j (array l 1 (replicate (Z.to_nat n) v))) Î”' = Some Î”'' âˆ§
     envs_entails Î”'' (WP fill K (Val $ LitV $ LitLoc l) @ s; E {{ Î¦ }})) â†’
   envs_entails Î” (WP fill K (AllocN (Val $ LitV $ LitInt n) (Val v)) @ s; E {{ Î¦ }}).
 Proof.
@@ -200,7 +200,7 @@ Qed.
 Lemma tac_twp_allocN Î” s E j K v n Î¦ :
   0 < n â†’
   (âˆ€ l, âˆƒ Î”',
-    envs_app false (Esnoc Enil j (array l (replicate (Z.to_nat n) v))) Î”
+    envs_app false (Esnoc Enil j (array l 1 (replicate (Z.to_nat n) v))) Î”
     = Some Î”' âˆ§
     envs_entails Î”' (WP fill K (Val $ LitV $ LitLoc l) @ s; E [{ Î¦ }])) â†’
   envs_entails Î” (WP fill K (AllocN (Val $ LitV $ LitInt n) (Val v)) @ s; E [{ Î¦ }]).