Setoid injectivity of Some.

cfb3f5f5 · Robbert Krebbers · 596a0a2c · cfb3f5f5
Commit cfb3f5f5 authored Sep 20, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 0 deletions

theories/option.v theories/option.v +2 -0

No files found.
--- 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.