From cfb3f5f5954a09c5663b1c8ff52c4b88478a3e81 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Sep 2016 23:18:15 +0200
Subject: [PATCH] Setoid injectivity of Some.

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

diff --git a/theories/option.v b/theories/option.v
index 5f1508e3..004ef002 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -118,6 +118,8 @@ Section setoids.
   Proof. apply _. Qed.
   Global Instance Some_proper : Proper ((≡) ==> (≡)) (@Some A).
   Proof. by constructor. Qed.
+  Global Instance Some_equiv_inj : Inj (≡) (≡) (@Some A).
+  Proof. by inversion_clear 1. Qed.
   Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
   Proof. intros x y; destruct 1; fold_leibniz; congruence. Qed.
 
-- 
GitLab