From 26be4a4b7b4ca319812b0cdd0895b9ccd501fd84 Mon Sep 17 00:00:00 2001
From: Vincent <vincent.siles@ens-lyon.org>
Date: Tue, 16 Nov 2021 19:46:53 +0000
Subject: [PATCH] Adding gmap_fmap_ext_ne

---
 iris/algebra/gmap.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 7a7c56546..7db23d421 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -656,6 +656,15 @@ End unital_properties.
 Global Instance gmap_fmap_ne `{Countable K} {A B : ofe} (f : A → B) n :
   Proper (dist n ==> dist n) f → Proper (dist n ==>dist n) (fmap (M:=gmap K) f).
 Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
+Lemma gmap_fmap_ne_ext `{Countable K}
+  {A : Type} {B : ofe} (f1 f2 : A → B) (m : gmap K A) n :
+  (∀ i x, m !! i = Some x → f1 x ≡{n}≡ f2 x) →
+  f1 <$> m ≡{n}≡ f2 <$> m.
+Proof.
+  move => Hf i.
+  rewrite !lookup_fmap.
+  destruct (m !! i) eqn:?; constructor; by eauto.
+Qed.
 Global Instance gmap_fmap_cmra_morphism `{Countable K} {A B : cmra} (f : A → B)
   `{!CmraMorphism f} : CmraMorphism (fmap f : gmap K A → gmap K B).
 Proof.
-- 
GitLab