From c2e4e322947db48ac80a24560308ba6bffa12172 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.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 775fbbd3..6ee84131 100644
--- a/theories/fin_maps.v
+++ b/theories/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