WhoCites Definitions DiscrMathExt Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites int nzero?
int_nzeroDef   == {i:i  0 }
Thm*    Type
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

Syntax: has structure: int_nzero

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

WhoCites Definitions DiscrMathExt Sections NuprlLIB Doc