From 5cd8f9cd475bc26ff610fbbe1e3f4b3338f4a607 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 7 Nov 2017 23:44:48 -0500
Subject: Add option_map_map

---
 src/Util/Option.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'src/Util/Option.v')

diff --git a/src/Util/Option.v b/src/Util/Option.v
index 5544fa428..a7b9df4e1 100644
--- a/src/Util/Option.v
+++ b/src/Util/Option.v
@@ -68,6 +68,12 @@ Proof.
   destruct v; reflexivity.
 Qed.
 
+Lemma option_map_map : forall {A B C} (f:A->B) (g:B->C) v,
+    option_map g (option_map f v) = option_map (fun v => g (f v)) v.
+Proof.
+  destruct v; reflexivity.
+Qed.
+
 Lemma option_rect_function {A B C S' N' v} f
   : f (option_rect (fun _ : option A => option B) S' N' v)
     = option_rect (fun _ : option A => C) (fun x => f (S' x)) (f N') v.
-- 
cgit v1.2.3