From ddd24bdc047eae3a15ec2421bc80a15fcaee9eb5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 14 Mar 2021 14:17:17 +0100
Subject: [PATCH] Add lemma `map_difference_right_id`

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index c861db2d..bab9041d 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2387,12 +2387,9 @@ Proof.
   apply map_empty; intros i. rewrite lookup_difference_None.
   destruct (m !! i); eauto.
 Qed.
+Global Instance map_difference_right_id {A} : RightId (=) (∅:M A) (∖) := _.
 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.
+Proof. by rewrite (right_id _ _). Qed.
 End theorems.
 
 (** ** The seq operation *)
-- 
GitLab