From 2a2fd26556006cef03a35d46719b014ef3862a62 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 14 Mar 2021 13:29:15 +0100
Subject: [PATCH] add delete_insert_union

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 4e7ae1fc..e149e0c1 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2104,6 +2104,13 @@ Qed.
 Lemma delete_union {A} (m1 m2 : M A) i :
   delete i (m1 ∪ m2) = delete i m1 ∪ delete i m2.
 Proof. apply delete_union_with. Qed.
+Lemma delete_insert_union {A} (m1 m2 : M A) i x :
+  m1 !! i = Some x ->
+  delete i m1 ∪ <[i := x]> m2 = m1 ∪ m2.
+Proof.
+  intros Hmi. rewrite <-insert_union_r by apply lookup_delete.
+  rewrite insert_union_l, insert_delete, insert_id; done.
+Qed.
 Lemma map_Forall_union_1_1 {A} (m1 m2 : M A) P :
   map_Forall P (m1 ∪ m2) → map_Forall P m1.
 Proof. intros HP i x ?. apply HP, lookup_union_Some_raw; auto. Qed.
-- 
GitLab