Definitions NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
geDef ij == ji
Thm* i,j:. (ij Prop
gtDef i>j == j<i
Thm* i,j:. (i>j Prop
iffDef P  Q == (P  Q) & (P  Q)
Thm* A,B:Prop. (A  B Prop
leDef AB == B<A
Thm* i,j:. (ij Prop
nequalDef a  b  T == a = b  T
Thm* A:Type, x,y:A. (x  y Prop
notDef A == A  False
Thm* A:Prop. (A Prop

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

Definitions NuprlPrimitives Sections NuprlLIB Doc