diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index ab01036cbd06204aa8c0283018de14b8a717a836..a6211d3eefa59811f2f097137b80e0f6b4524091 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2966,7 +2966,7 @@ Proof.
 Qed.
 End theorems.
 
-(** ** The seq operation *)
+(** ** The [map_seq] operation *)
 Section map_seq.
   Context `{FinMap nat M} {A : Type}.
   Implicit Types x : A.
@@ -3054,6 +3054,16 @@ Section map_seq.
     { by rewrite fmap_empty. }
     by rewrite fmap_insert, IH.
   Qed.
+
+  Lemma insert_map_seq_0 (xs : list A) i x:
+    i < length xs →
+    <[i:=x]> (map_seq (M:=M A) 0 xs) = map_seq 0 (<[i:=x]> xs).
+  Proof.
+    intros ?. apply map_eq. intros j. rewrite lookup_map_seq_0.
+    destruct (decide (i = j)) as [->|Hne].
+    - rewrite lookup_insert, list_lookup_insert; done.
+    - rewrite lookup_insert_ne, lookup_map_seq_0, list_lookup_insert_ne; done.
+  Qed.
 End map_seq.
 
 Section kmap.