Def  a  b  T == a = b  T

is mentioned by

Thm*  p:. prime(p)  (b,z:. p | zb  b  0 & p | z)	[prime_divs_exp]
Thm*  x,y:. x  y  trivial_factorization(x)(y) = 0	[trivial_factorization_comp2]

In prior sections: int 1 bool 1 int 2

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