From 82d4b44849d843c73b4067d1bcd48e73ac222bd8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 26 Feb 2016 21:04:35 +0100
Subject: [PATCH] Lemma for validity of Some.

---
 algebra/option.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/algebra/option.v b/algebra/option.v
index f0a5d5f66..96e53f851 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -72,6 +72,7 @@ Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
 Instance option_minus : Minus (option A) :=
   difference_with (λ x y, Some (x ⩪ y)).
 
+Definition Some_valid a : ✓ Some a ↔ ✓ a := reflexivity _.
 Definition Some_op a b : Some (a â‹… b) = Some a â‹… Some b := eq_refl.
 
 Lemma option_included (mx my : option A) :
-- 
GitLab