Library mathcomp.ssreflect.ssrfun
Lemma
Some_inj
{
T
:
nonPropType
} :
injective
(@
Some
T
).