WhoCites Definitions StandardLib Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites pm equal?
pm_equalDef i =  j == i = j    i = -j
Thm* a,b:a =  b  Prop

Syntax:i =  j has structure: pm_equal(ij)

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

WhoCites Definitions StandardLib Sections NuprlLIB Doc