From 3cda390bf0c5714c12a7e0cda51cc275c7f8b033 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 13 Feb 2016 21:01:06 +0100
Subject: [PATCH] Extensionality of omap.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 1699bd0e..071b832a 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -558,6 +558,12 @@ Proof.
   intros Hi; apply map_eq; intros i; rewrite !lookup_fmap.
   by destruct (m !! i) eqn:?; simpl; erewrite ?Hi by eauto.
 Qed.
+Lemma omap_ext {A B} (f1 f2 : A → option B) m :
+  (∀ i x, m !! i = Some x → f1 x = f2 x) → omap f1 m = omap f2 m.
+Proof.
+  intros Hi; apply map_eq; intros i; rewrite !lookup_omap.
+  by destruct (m !! i) eqn:?; simpl; erewrite ?Hi by eauto.
+Qed.
 
 (** ** Properties of conversion to lists *)
 Lemma map_to_list_unique {A} (m : M A) i x y :
-- 
GitLab