From 4ad4a8c3b3b89122dfca5b194cc00f5308b56c2a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 17 Feb 2016 12:55:08 +0100
Subject: [PATCH] Misc map_to_list properties.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 77aea823..10e76cdf 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -671,6 +671,12 @@ Proof.
     rewrite elem_of_map_to_list in Hlookup. congruence.
   - by rewrite !map_of_to_list.
 Qed.
+Lemma map_to_list_contains {A} (m1 m2 : M A) :
+  m1 ⊆ m2 → map_to_list m1 `contains` map_to_list m2.
+Proof.
+  intros; apply NoDup_contains; auto using NoDup_map_to_list.
+  intros [i x]. rewrite !elem_of_map_to_list; eauto using lookup_weaken.
+Qed.
 Lemma map_of_list_nil {A} : map_of_list (@nil (K * A)) = ∅.
 Proof. done. Qed.
 Lemma map_of_list_cons {A} (l : list (K * A)) i x :
-- 
GitLab