Def  1-1 xA,yB. R(x;y)
Def  == x,x':A, y,y':B. R(x;y) & R(x';y')  (x = x'  y = y')

is mentioned

In prior sections: DiscreteMath

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