From 36bfee17a80e00f9a675122f73f77d30ad7df262 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 16 Jan 2016 01:29:43 +0100
Subject: [PATCH] More option properties.

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

diff --git a/theories/option.v b/theories/option.v
index 237194c2..865311fd 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -107,6 +107,8 @@ Section setoids.
   Lemma equiv_Some (mx my : option A) x :
     mx â‰¡ my â†’ mx = Some x â†’ âˆƒ y, my = Some y âˆ§ x â‰¡ y.
   Proof. destruct 1; naive_solver. Qed.
+  Global Instance is_Some_proper : Proper ((â‰¡) ==> iff) (@is_Some A).
+  Proof. inversion_clear 1; split; eauto. Qed.
 End setoids.
 
 (** Equality on [option] is decidable. *)
-- 
GitLab