From 8fdeb77fffe73d3820a656027a150b493944a3c0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 14 May 2018 20:45:52 +0200
Subject: [PATCH] =?UTF-8?q?Prove=20`m=20=E2=88=96=20m=20=3D=20=E2=88=85`?=
 =?UTF-8?q?=20for=20finite=20maps.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index d53ea324..bcce9efd 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1884,6 +1884,11 @@ Proof.
   destruct (m1 !! i) as [x'|], (m2 !! i);
     try specialize (Hm1m2 x'); compute; intuition congruence.
 Qed.
+Lemma map_difference_diag {A} (m : M A) : m ∖ m = ∅.
+Proof.
+  apply map_empty; intros i. rewrite lookup_difference_None.
+  destruct (m !! i); eauto.
+Qed.
 End theorems.
 
 (** * Tactics *)
-- 
GitLab