WhoCites Definitions FTA 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(Tab)

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

WhoCites Definitions FTA Sections DiscrMathExt Doc