Commit 54ede303 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Setoid injectivity of Some.

parent a5e657c3
...@@ -118,6 +118,8 @@ Section setoids. ...@@ -118,6 +118,8 @@ Section setoids.
Proof. apply _. Qed. Proof. apply _. Qed.
Global Instance Some_proper : Proper (() ==> ()) (@Some A). Global Instance Some_proper : Proper (() ==> ()) (@Some A).
Proof. by constructor. Qed. 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). Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
Proof. intros x y; destruct 1; fold_leibniz; congruence. Qed. Proof. intros x y; destruct 1; fold_leibniz; congruence. Qed.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment