From 5acbf5030a141410f59d5ec6c709945e4e889b02 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 4 Dec 2020 19:41:34 +0100
Subject: [PATCH] add insert_subseteq_l

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index a5aa829c..bfbc2eeb 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -567,6 +567,13 @@ Lemma insert_subseteq_r {A} (m1 m2 : M A) i x :
 Proof.
   intros. trans (<[i:=x]> m1); eauto using insert_subseteq, insert_mono.
 Qed.
+Lemma insert_subseteq_l {A} (m1 m2 : M A) i x :
+  m2 !! i = Some x → m1 ⊆ m2 → <[i:=x]> m1 ⊆ m2.
+Proof.
+  intros Hi Hincl. replace m2 with (<[i:=x]> m2).
+  - apply insert_mono. done.
+  - apply insert_id. done.
+Qed.
 
 Lemma insert_delete_subseteq {A} (m1 m2 : M A) i x :
   m1 !! i = None → <[i:=x]> m1 ⊆ m2 → m1 ⊆ delete i m2.
-- 
GitLab