Def a  b  T == a = b  T

is mentioned by

Thm* a,b:. a  0  b  0  ab  0

[int_entire_a]

In prior sections: int 1 bool 1

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html