Library mathcomp.ssreflect.ssrfun
Local additions: void == a notation for the Empty_set type of the standard library. of_void T == the canonical injection void -> T.
Lemma
Some_inj
{
T
:
nonPropType
} :
injective
(@
Some
T
).
Notation
void
:=
Empty_set
.
Definition
of_void
T
(
x
:
void
) :
T
:=
match
x
with
end
.
Lemma
of_voidK
T
:
pcancel
(
of_void
T
)
[
fun
_
⇒
None
]
.
Lemma
inj_compr
A
B
C
(
f
:
B
→
A
) (
h
:
C
→
B
) :
injective
(
f
\
o
h
)
→
injective
h
.