IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
When two expressions are simply the result of renaming binding variables, they are sometimes said to be "-equivalent". For example,
(x:. y:. x<y)
is -equivalent to
(u:. x:. u<x)
They are sometimes also called "identical modulo change of bound variables."
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
x:
. 
y:
-equivalent to
