From abe0ec66a188c48cd6f86565e6fc5cfc784727bd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 4 Jan 2021 23:11:44 +0100
Subject: [PATCH] Add lemma `bind_Some_equiv`.

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

diff --git a/theories/option.v b/theories/option.v
index cd88494a..f2eed50f 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -225,6 +225,9 @@ Proof. intros. by apply option_bind_ext. Qed.
 Lemma bind_Some {A B} (f : A â†’ option B) (mx : option A) y :
   mx â‰«= f = Some y â†” âˆƒ x, mx = Some x âˆ§ f x = Some y.
 Proof. destruct mx; naive_solver. Qed.
+Lemma bind_Some_equiv {A} `{Equiv B} (f : A â†’ option B) (mx : option A) y :
+  mx â‰«= f â‰¡ Some y â†” âˆƒ x, mx = Some x âˆ§ f x â‰¡ Some y.
+Proof. destruct mx; (split; [inversion 1|]); naive_solver. Qed.
 Lemma bind_None {A B} (f : A â†’ option B) (mx : option A) :
   mx â‰«= f = None â†” mx = None âˆ¨ âˆƒ x, mx = Some x âˆ§ f x = None.
 Proof. destruct mx; naive_solver. Qed.
-- 
GitLab