WhoCites
Definitions
LogicSupplement
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(
x
is the unique
A
such that
P
(
x
)
)
Who Cites is
the?
is_the
Def
x
is the
u
:
A
.
P
(
u
) ==
P
(
x
) & (
u
:
A
.
P
(
u
)
u
=
x
)
Thm*
A
:Type,
P
:(
A
Prop),
x
:
A
. (x is the
x
:
A
.
P
(
x
))
Prop
Syntax:
x
is the
u
:
A
.
P
(
u
)
has structure:
is_the(
x
;
A
;
u
.
P
(
u
))
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
LogicSupplement
Sections
DiscrMathExt
Doc
u:A. P(u) 
u = x)A:Type, P:(A
Prop), x:A. (x is the x:A. P(x)) 
Propu:A. P(u) u = x)A:Type, P:(AProp), x:A. (x is the x:A. P(x)) Prop
