From a7f54bc47a8490fde2a078d05adeff02ba31c29d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 16 Jan 2018 23:47:00 +0100
Subject: [PATCH] Add `fmap_Some_1` and `fmap_Some_2`.

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

diff --git a/theories/option.v b/theories/option.v
index 59b6b7b3..f539f4bf 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -183,6 +183,11 @@ Proof. unfold is_Some; destruct mx; naive_solver. Qed.
 Lemma fmap_Some {A B} (f : A → B) mx y :
   f <$> mx = Some y ↔ ∃ x, mx = Some x ∧ y = f x.
 Proof. destruct mx; naive_solver. Qed.
+Lemma fmap_Some_1 {A B} (f : A → B) mx y :
+  f <$> mx = Some y → ∃ x, mx = Some x ∧ y = f x.
+Proof. apply fmap_Some. Qed.
+Lemma fmap_Some_2 {A B} (f : A → B) mx x : mx = Some x → f <$> mx = Some (f x).
+Proof. intros. apply fmap_Some; eauto. Qed.
 Lemma fmap_Some_equiv {A B} `{Equiv B} `{!Equivalence ((≡) : relation B)}
       (f : A → B) mx y :
   f <$> mx ≡ Some y ↔ ∃ x, mx = Some x ∧ y ≡ f x.
-- 
GitLab