From a01453ed6b6e155b89932f307fb8c3e1cff7cf2d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 23 Sep 2016 13:59:39 +0200
Subject: [PATCH] Relate map_to_list to nil.

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

diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index 475777ffd..229dfcd75 100644
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -707,6 +707,11 @@ Lemma map_to_list_empty_inv_alt {A}  (m : M A) : map_to_list m ≡ₚ [] → m =
 Proof. rewrite <-map_to_list_empty. apply map_to_list_inj. Qed.
 Lemma map_to_list_empty_inv {A} (m : M A) : map_to_list m = [] → m = ∅.
 Proof. intros Hm. apply map_to_list_empty_inv_alt. by rewrite Hm. Qed.
+Lemma map_to_list_empty' {A} (m : M A) : map_to_list m = [] ↔ m = ∅.
+Proof.
+  split. apply map_to_list_empty_inv. intros ->. apply map_to_list_empty.
+Qed.
+
 Lemma map_to_list_insert_inv {A} (m : M A) l i x :
   map_to_list m ≡ₚ (i,x) :: l → m = <[i:=x]>(map_of_list l).
 Proof.
-- 
GitLab