diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 4f55ecbdd9dae773c8dc1b9b0d94a5b4fa075c56..9d7f906bb5d582fc82a734b2f9b7371886889747 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -155,6 +155,12 @@ Section tests.
     by iApply "HΦ".
   Qed.
 
+  Lemma test_array_app l vs1 vs2 :
+    l ↦∗ (vs1 ++ vs2) -∗ l ↦∗ (vs1 ++ vs2).
+  Proof.
+    iIntros "[H1 H2]". iSplitL "H1"; done.
+  Qed.
+
 End tests.
 
 Section printing_tests.
diff --git a/theories/heap_lang/array.v b/theories/heap_lang/array.v
index d046a9932fff426b2bb6010bc7ed69a11c2788f0..c7dee76969db036a68a8b42a2def4710bc65d3c8 100644
--- a/theories/heap_lang/array.v
+++ b/theories/heap_lang/array.v
@@ -61,6 +61,25 @@ Proof.
   rewrite drop_insert; last by lia. done.
 Qed.
 
+(** Proofmode instances *)
+Global Instance into_sep_array_cons l vs v vs' :
+  IsCons vs v vs' →
+  IntoSep (l ↦∗ vs) (l ↦ v) ((l +ₗ 1) ↦∗ vs').
+Proof. rewrite /IsCons=>->. by rewrite /IntoSep array_cons. Qed.
+Global Instance into_sep_array_app l vs vs1 vs2 :
+  IsApp vs vs1 vs2 →
+  IntoSep (l ↦∗ vs) (l ↦∗ vs1) ((l +ₗ length vs1) ↦∗ vs2).
+Proof. rewrite /IsApp=>->. by rewrite /IntoSep array_app. Qed.
+
+Global Instance from_sep_array_cons l vs v vs' :
+  IsCons vs v vs' →
+  FromSep (l ↦∗ vs) (l ↦ v) ((l +ₗ 1) ↦∗ vs').
+Proof. rewrite /IsCons=> ->. by rewrite /FromSep array_cons. Qed.
+Global Instance from_sep_array_app l vs vs1 vs2 :
+  IsApp vs vs1 vs2 →
+  FromSep (l ↦∗ vs) (l ↦∗ vs1) ((l +ₗ length vs1) ↦∗ vs2).
+Proof. rewrite /IsApp=> ->. by rewrite /FromSep array_app. Qed.
+
 (** Allocation *)
 Lemma mapsto_seq_array l v n :
   ([∗ list] i ∈ seq 0 n, (l +ₗ (i : nat)) ↦ v) -∗