From 0a7cb77057583d2e2e8cd30e3ec6a56e844012ef Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 14 Mar 2021 14:05:23 +0100
Subject: [PATCH] add map_difference_empty

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 7e60989a..67d77eaf 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2380,6 +2380,12 @@ Proof.
   apply map_empty; intros i. rewrite lookup_difference_None.
   destruct (m !! i); eauto.
 Qed.
+Lemma map_difference_empty {A} (m : M A) : m ∖ ∅ = m.
+Proof.
+  apply map_eq. intros i. apply option_eq. intros x.
+  rewrite lookup_difference_Some. rewrite lookup_empty.
+  naive_solver.
+Qed.
 End theorems.
 
 (** ** The seq operation *)
-- 
GitLab