From 187db929ebca3087c4589a6b690da7eb292fd87e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 21 Dec 2015 14:26:41 +0100
Subject: [PATCH] Something close to non-expansiveness of is_Some.

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

diff --git a/modures/option.v b/modures/option.v
index abb627e00..aec24387a 100644
--- a/modures/option.v
+++ b/modures/option.v
@@ -49,6 +49,8 @@ Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed.
 Instance option_fmap_ne `{Dist A, Dist B} (f : A → B) n:
   Proper (dist n ==> dist n) f → Proper (dist n==>dist n) (fmap (M:=option) f).
 Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.
+Instance is_Some_ne `{Dist A} : Proper (dist (S n) ==> iff) (@is_Some A).
+Proof. intros n; inversion_clear 1; split; eauto. Qed.
 
 (* CMRA *)
 Instance option_valid `{Valid A} : Valid (option A) := λ mx,
-- 
GitLab