diff --git a/algebra/option.v b/algebra/option.v
index f0a5d5f6677ff6a15d10c2b901c57ff30d07a9b7..96e53f851b4c45d7ee08c2beffaa4d36a1f14781 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) :