diff --git a/theories/heap_lang/array.v b/theories/heap_lang/array.v
index 415f1cb76de584a655fbb42ef695fcc39ab19abf..15331b9e8f1cd5f3726207ab93a69dcef1907f14 100644
--- a/theories/heap_lang/array.v
+++ b/theories/heap_lang/array.v
@@ -28,6 +28,8 @@ Implicit Types vs : list val.
 Implicit Types l : loc.
 Implicit Types sz off : nat.
 
+Global Instance array_timeless l vs : Timeless (array l vs) := _.
+
 Lemma array_nil l : l ↦∗ [] ⊣⊢ emp.
 Proof. by rewrite /array. Qed.