From f6b0626bd542b70845aca65ead6164cca0390344 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.

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

diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index 5df84b288..cb296d38e 100644
--- a/prelude/fin_maps.v
+++ b/prelude/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