IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def Preorder(T;x,y.R(x;y)) == Refl(T;x,y.R(x;y)) & (Trans x,y:T. R(x;y))
is mentioned
In prior sections:
rel 1
num thy 1
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
