Definitions LogicSupplement Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
iffDef  P  Q == (P  Q) & (P  Q)
Thm*  A,B:Prop. (A  B Prop
notDef  A == A  False
Thm*  A:Prop. (A Prop
squashDef  T == {:True| T }
Thm*  A:Prop. A  Prop

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

Definitions LogicSupplement Sections DiscrMathExt Doc