From 8d59d7a530dcc587837b3b8854153132b024fb1c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 10 Aug 2023 08:51:31 +0200
Subject: [PATCH] add option_fmap_dist_inj lemma

---
 iris/algebra/ofe.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 82d6cf079..bf8dc1550 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -1330,6 +1330,10 @@ Proof.
     apply optionO_map_ne, oFunctor_map_contractive.
 Qed.
 
+Global Instance option_fmap_dist_inj {A B : ofe} (f : A → B) n :
+  Inj (≡{n}≡) (≡{n}≡) f → Inj (≡{n}@{option A}≡) (≡{n}@{option B}≡) (fmap f).
+Proof. apply option_fmap_inj. Qed.
+
 (** * Later type *)
 (** Note that the projection [later_car] is not non-expansive (see also the
 lemma [later_car_anti_contractive] below), so it cannot be used in the logic.
-- 
GitLab