From d6b324535b5b6e54d4784a67019a3a231a541b5c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 14 Mar 2021 13:50:53 +0100
Subject: [PATCH] add map_empty_subseteq

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index e149e0c1..7e60989a 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -296,6 +296,8 @@ Lemma map_subset_empty {A} (m : M A) : m ⊄ ∅.
 Proof.
   intros [_ []]. rewrite map_subseteq_spec. intros ??. by rewrite lookup_empty.
 Qed.
+Lemma map_empty_subseteq {A} (m : M A) : ∅ ⊆ m.
+Proof. apply map_subseteq_spec. intros k v []%lookup_empty_Some. Qed.
 
 Lemma map_subset_alt {A} (m1 m2 : M A) :
   m1 ⊂ m2 ↔ m1 ⊆ m2 ∧ ∃ i, m1 !! i = None ∧ is_Some (m2 !! i).
-- 
GitLab