IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
int seg well founded down2 1. i : 2. j : {i...}
3. WellFnd{u}({i..j};x,y.j+i-x<j+i-y)
WellFnd{u}({i..j};x,y.x>y)
By:
Rewrite by x,y:. j+i-x<j+i-yx>y
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
};x,y.j+i-x<j+i-y)
WellFnd{u}({i..j
x,y:
x>y
