Library mathcomp.ssreflect.ssrfun


Lemma Some_inj {T : nonPropType} : injective (@Some T).