From 1a21e90812e76953856b175faac098e8eb445bb7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 30 Jun 2018 10:12:25 +0200
Subject: [PATCH] Lemma list_insert_id.

---
 theories/list.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index 87576f64..cc4254d5 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.
-- 
GitLab