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

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 7bb6d2fe..b887f0b6 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -177,6 +177,9 @@ Section setoid.
   Lemma map_equiv_lookup_l (m1 m2 : M A) i x :
     m1 ≡ m2 → m1 !! i = Some x → ∃ y, m2 !! i = Some y ∧ x ≡ y.
   Proof. generalize (equiv_Some_inv_l (m1 !! i) (m2 !! i) x); naive_solver. Qed.
+  Lemma map_equiv_lookup_r (m1 m2 : M A) i y :
+    m1 ≡ m2 → m2 !! i = Some y → ∃ x, m1 !! i = Some x ∧ x ≡ y.
+  Proof. generalize (equiv_Some_inv_r (m1 !! i) (m2 !! i) y); naive_solver. Qed.
 
   Global Instance map_equivalence : Equivalence (≡@{A}) → Equivalence (≡@{M A}).
   Proof.
-- 
GitLab