WhoCites Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites nequal?
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:a  b has structure: nequal(T; a; b)

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

WhoCites Definitions DiscreteMath Sections DiscrMathExt Doc