From bc227866e011c4d398f444b65fa1c62cfed3db0d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 4 Feb 2016 18:22:20 +0100
Subject: [PATCH] Extensionality for fmap on option.

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

diff --git a/theories/option.v b/theories/option.v
index bf66ba97..4a28e666 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -148,6 +148,12 @@ Proof. by destruct x. Qed.
 Lemma option_fmap_compose {A B} (f : A → B) {C} (g : B → C) x :
   g ∘ f <$> x = g <$> f <$> x.
 Proof. by destruct x. Qed.
+Lemma option_fmap_ext {A B} (f g : A → B) x :
+  (∀ y, f y = g y) → f <$> x = g <$> x.
+Proof. destruct x; simpl; auto with f_equal. Qed.
+Lemma option_fmap_setoid_ext `{Equiv A, Equiv B} (f g : A → B) x :
+  (∀ y, f y ≡ g y) → f <$> x ≡ g <$> x.
+Proof. destruct x; constructor; auto. Qed.
 Lemma option_fmap_bind {A B C} (f : A → B) (g : B → option C) x :
   (f <$> x) ≫= g = x ≫= g ∘ f.
 Proof. by destruct x. Qed.
-- 
GitLab