IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
upto iseg i,j:. ij upto(i) upto(j)
By:
Auto THEN Unfold `iseg` 0
THEN
Inst Thm*m:, n:(m+1). upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n))) [j;i]
THEN
HypSubst -1 0
THEN
InstConcl [map(x.x+i;upto(j-i))]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
i,j:
. i
j 
upto(i) 
x.x+n;upto(m-n))) [j;i]
