From d631fdde0728476935b7cbe6a6fc950573930de9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 9 Dec 2016 15:42:39 +0100
Subject: [PATCH] =?UTF-8?q?Rename=20fmap=5FSome=5Fequiv'=20=E2=86=92=20fma?=
 =?UTF-8?q?p=5FSome=5Fequiv=5F1.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

We typically use the _1 and _2 suffix to denote individual directions
of a lemmas that is a biimplication.
---
 theories/option.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/option.v b/theories/option.v
index 9e7c8896..73ae6eff 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -190,10 +190,10 @@ Proof.
   - intros ?%symmetry%equiv_None. done.
   - intros (? & ? & ?). done.
 Qed.
-Lemma fmap_Some_equiv' {A B} `{Equiv B} `{!Equivalence ((≡) : relation B)}
+Lemma fmap_Some_equiv_1 {A B} `{Equiv B} `{!Equivalence ((≡) : relation B)}
       (f : A → B) mx y :
   f <$> mx ≡ Some y → ∃ x, mx = Some x ∧ y ≡ f x.
-Proof. intros. apply fmap_Some_equiv. done. Qed.
+Proof. by rewrite fmap_Some_equiv. Qed.
 Lemma fmap_None {A B} (f : A → B) mx : f <$> mx = None ↔ mx = None.
 Proof. by destruct mx. Qed.
 Lemma option_fmap_id {A} (mx : option A) : id <$> mx = mx.
-- 
GitLab