From 6df1a64749ff3ff13871ee3faf9513946f912895 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 18 Nov 2021 15:40:30 +0100
Subject: [PATCH] Add lemma `map_subseteq_inv`.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 8b0a6ea3..b5d8197d 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2646,6 +2646,15 @@ Proof.
   by rewrite lookup_difference_Some, map_filter_lookup_Some.
 Qed.
 
+(** ** Misc properties about the order *)
+Lemma map_subseteq_inv {A} (m1 m2 : M A) : m1 ⊆ m2 → m1 ⊂ m2 ∨ m1 = m2.
+Proof.
+  intros. destruct (decide (m2 ∖ m1 = ∅)) as [Hm21|(i&x&Hi)%map_choose].
+  - right. by rewrite <-(map_difference_union m1 m2), Hm21, (right_id_L _ _).
+  - left. apply lookup_difference_Some in Hi as [??].
+    apply map_subset_alt; eauto.
+Qed.
+
 (** ** Setoids *)
 Section setoid.
   Context `{Equiv A}.
-- 
GitLab