From b5e1f0c8084c9ecb2bfa7e90a6d5163d3efa9ecb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 4 Nov 2020 17:23:38 +0100
Subject: [PATCH] add big_opM_singletons
---
theories/algebra/gmap.v | 9 +++++++++
1 file changed, 9 insertions(+)
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index ed15a0559..c2de82129 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -594,6 +594,15 @@ Proof.
intros ??. rewrite !lookup_included=> Hm i.
rewrite !lookup_fmap. by apply option_fmap_mono.
Qed.
+
+Lemma big_opM_singletons (m : gmap K A) :
+ ([^op map] k ↦ x ∈ m, {[ k := x ]}) ≡ m.
+Proof.
+ induction m as [|k x m Hk IH] using map_ind.
+ - rewrite big_opM_empty. done.
+ - rewrite big_opM_insert // IH insert_singleton_op //.
+Qed.
+
End properties.
Section unital_properties.
--
GitLab