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

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

diff --git a/theories/option.v b/theories/option.v
index b69d1dc3..82b1387a 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -179,6 +179,9 @@ Global Instance option_guard: MGuard option := λ P dec A f,
 Global Instance option_fmap_inj {A B} (f : A → B) :
   Inj (=) (=) f → Inj (=@{option A}) (=@{option B}) (fmap f).
 Proof. intros ? [x1|] [x2|] [=]; naive_solver. Qed.
+Global Instance option_fmap_equiv_inj `{Equiv A, Equiv B} (f : A → B) :
+  Inj (≡) (≡) f → Inj (≡@{option A}) (≡@{option B}) (fmap f).
+Proof. intros ? [x1|] [x2|]; inversion 1; subst; constructor; by apply (inj _). Qed.
 
 Lemma fmap_is_Some {A B} (f : A → B) mx : is_Some (f <$> mx) ↔ is_Some mx.
 Proof. unfold is_Some; destruct mx; naive_solver. Qed.
-- 
GitLab