diff --git a/theories/list.v b/theories/list.v
index 87576f64f11b96fa43d7d69c2d39616e60ae544e..cc4254d593206339ed84f6ad86b933f42ed28ddb 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -521,6 +521,9 @@ Qed.
 Lemma list_insert_commute l i j x y :
   i ≠ j → <[i:=x]>(<[j:=y]>l) = <[j:=y]>(<[i:=x]>l).
 Proof. revert i j. by induction l; intros [|?] [|?] ?; f_equal/=; auto. Qed.
+Lemma list_insert_id l i x : l !! i = Some x → <[i:=x]>l = l.
+Proof. revert i. induction l; intros [|i] [=]; f_equal/=; auto. Qed.
+
 Lemma list_lookup_other l i x :
   length l ≠ 1 → l !! i = Some x → ∃ j y, j ≠ i ∧ l !! j = Some y.
 Proof.