From a4dc90a9d0880e148e72d35767c27f654fe9554f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 3 Jul 2021 12:55:17 +0200
Subject: [PATCH] add lookup_union_l

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index b163bef2..6295991c 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1988,6 +1988,9 @@ Proof. apply lookup_union_with. Qed.
 Lemma lookup_union_r {A} (m1 m2 : M A) i :
   m1 !! i = None → (m1 ∪ m2) !! i = m2 !! i.
 Proof. intros Hi. by rewrite lookup_union, Hi, (left_id_L _ _).  Qed.
+Lemma lookup_union_l {A} (m1 m2 : M A) i :
+  is_Some (m1 !! i) → (m1 ∪ m2) !! i = m1 !! i.
+Proof. intros [x Hi]. rewrite lookup_union, Hi. by destruct (m2 !! i). Qed.
 Lemma lookup_union_Some_raw {A} (m1 m2 : M A) i x :
   (m1 ∪ m2) !! i = Some x ↔
     m1 !! i = Some x ∨ (m1 !! i = None ∧ m2 !! i = Some x).
-- 
GitLab