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