From 65def9bb2db4c632290aed236e5d35b7f549ceb7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 14 Mar 2021 15:04:41 +0100
Subject: [PATCH] 'delete' is map-specific, no need for 'map' prefix

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 654c7acf..577a3c07 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2394,14 +2394,14 @@ Global Instance map_difference_right_id {A} : RightId (=) (∅:M A) (∖) := _.
 Lemma map_difference_empty {A} (m : M A) : m ∖ ∅ = m.
 Proof. by rewrite (right_id _ _). Qed.
 
-Lemma map_delete_difference {A} (m1 m2 : M A) i x :
+Lemma delete_difference {A} (m1 m2 : M A) i x :
   delete i (m1 ∖ m2) = m1 ∖ <[i:=x]> m2.
 Proof.
   apply map_eq. intros j. apply option_eq. intros y.
   rewrite lookup_delete_Some, !lookup_difference_Some, lookup_insert_None.
   naive_solver.
 Qed.
-Lemma map_difference_delete {A} (m1 m2 : M A) i x :
+Lemma difference_delete {A} (m1 m2 : M A) i x :
   m1 !! i = Some x →
   m1 ∖ delete i m2 = <[i:=x]> (m1 ∖ m2).
 Proof.
-- 
GitLab