Library Coq.Logic.StrictProp
Utilities for SProp users.
Record
Box
(
A
:
SProp
) :
Prop
:=
box
{
unbox
:
A
}.
Arguments
box
{
_
}
_
.
Arguments
unbox
{
_
}
_
.
Inductive
Squash
(
A
:
Type
) :
SProp
:=
squash
:
A
->
Squash
A
.
Arguments
squash
{
_
}
_
.
Inductive
sEmpty
:
SProp
:=.
Inductive
sUnit
:
SProp
:=
stt
.
Record
Ssig
{
A
:
Type
} (
P
:
A
->
SProp
) :=
Sexists
{
Spr1
:
A
;
Spr2
:
P
Spr1
}.
Arguments
Sexists
{
_
}
_
_
_
.
Arguments
Spr1
{
_
_
}
_
.
Arguments
Spr2
{
_
_
}
_
.
Lemma
Spr1_inj
{
A
P
} {
a
b
: @
Ssig
A
P
} (
e
:
Spr1
a
=
Spr1
b
) :
a
=
b
.