Definitions LogicSupplement Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
exteqDef  A =ext B == (x:Ax  B) & (x:Bx  A)
singletonDef  {a:T} == {x:Tx = a  T }
Thm*  T:Type, a:T. {a:T Type

About:
setuniverseequalmemberandall!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions LogicSupplement Sections DiscrMathExt Doc