From d5a2cd143b3b10b899ef124dfff5264a5db514d6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 9 Jun 2021 01:34:44 +0200
Subject: [PATCH] Add lemma `map_equiv_iff`.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index a109d858..7bb6d2fe 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -166,6 +166,8 @@ Context `{FinMap K M}.
 Section setoid.
   Context `{Equiv A}.
 
+  Lemma map_equiv_iff (m1 m2 : M A) : m1 ≡ m2 ↔ ∀ i, m1 !! i ≡ m2 !! i.
+  Proof. done. Qed.
   Lemma map_equiv_empty (m : M A) : m ≡ ∅ ↔ m = ∅.
   Proof.
     split; [intros Hm; apply map_eq; intros i|intros ->].
-- 
GitLab