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)
iffDef  P  Q == (P  Q) & (P  Q)
Thm*  A,B:Prop. (A  B Prop
squashDef  T == {:True| T }
Thm*  A:Prop. A  Prop
subtypeDef  S  T == x:Sx  T

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

Definitions LogicSupplement Sections DiscrMathExt Doc