From af8c793f2f22b07b75d3721e2161b81f9529fd3c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Nov 2016 11:39:38 +0100
Subject: [PATCH] Prove map_to_list {[i:=x]} = [(i,x)].

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

diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index 9e43bd240..91b8aebb7 100644
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -687,6 +687,12 @@ Proof.
     rewrite elem_of_map_to_list in Hlookup. congruence.
   - by rewrite !map_of_to_list.
 Qed.
+Lemma map_to_list_singleton {A} i (x : A) : map_to_list {[i:=x]} = [(i,x)].
+Proof.
+  apply Permutation_singleton. unfold singletonM, map_singleton.
+  by rewrite map_to_list_insert, map_to_list_empty by auto using lookup_empty.
+Qed.
+
 Lemma map_to_list_contains {A} (m1 m2 : M A) :
   m1 ⊆ m2 → map_to_list m1 `contains` map_to_list m2.
 Proof.
-- 
GitLab