From 14fe8208b0702644f56927b6212d13fda6840add Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 14 Feb 2016 21:57:19 +0100
Subject: [PATCH] Inserting into a fin_map twice.

---
 prelude/fin_maps.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index 220f183f8..5aee3f6c1 100644
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -403,6 +403,8 @@ Lemma lookup_insert_rev {A}  (m : M A) i x y : <[i:=x]>m !! i = Some y → x = y
 Proof. rewrite lookup_insert. congruence. Qed.
 Lemma lookup_insert_ne {A} (m : M A) i j x : i ≠ j → <[i:=x]>m !! j = m !! j.
 Proof. unfold insert. apply lookup_partial_alter_ne. Qed.
+Lemma insert_insert {A} (m : M A) i x y : <[i:=x]>(<[i:=y]>m) = <[i:=x]>m.
+Proof. unfold insert, map_insert. by rewrite <-partial_alter_compose. Qed.
 Lemma insert_commute {A} (m : M A) i j x y :
   i ≠ j → <[i:=x]>(<[j:=y]>m) = <[j:=y]>(<[i:=x]>m).
 Proof. apply partial_alter_commute. Qed.
-- 
GitLab