Def a  b  T == a = b  T

is mentioned by

Thm* (x.x)  (x.if x<0 0 ; x fi)	[sfa_doc_fun_noteq_example1]
Thm* P  Q  (x:. (x = 0  P) & (x  0  Q))	[sfa_doc_or_dec]
Thm* s:Sexpr(A). Size(s)  1    Size(sexprCdr(s))<Size(s)	[sfa_doc_sexprcdrsize]
Thm* s:Sexpr(A). Size(s)  1    Size(sexprCar(s))<Size(s)	[sfa_doc_sexprcarsize]

In prior sections: int 1 bool 1 int 2 sqequal 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html