Def P  Q == P+Q

is mentioned by

Thm* m,n:, f:({m..n}T). n<m  ||f{m..n}|| = n-m

[listify_length]

In prior sections: core bool 1 int 2

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