IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nat prod one iff factors one4 1. x,y:. xy = 1 y = 1
2. x : 3. y : 4. x = 1
5. y = 1
xy = 1
By:
Rewrite by x = 1
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
x,y:
. x
y = 1 
y = 1
x
