Definitions
LogicSupplement
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
exteq
Def
A
=ext
B
== (
x
:
A
.
x
B
) & (
x
:
B
.
x
A
)
singleton
Def
{
a
:
T
} == {
x
:
T
|
x
=
a
T
}
Thm*
T
:Type,
a
:
T
. {
a
:
T
}
Type
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
LogicSupplement
Sections
DiscrMathExt
Doc
x:A. x 
B) & (x:B. x A) T }T:Type, a:T. {a:T} Typex:A. x B) & (x:B. x A) T }T:Type, a:T. {a:T} Type
