IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
last l interval1 1. T : Type
2. l : T List
3. i : ||l||
4. j : i 5. ||l_interval(l;j;i)|| = i-j l[(j+i-j-1)] = l[(i-1)]
By:
ArithSimp 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
||l||
l[(j+i-j-1)] = l[(i-1)]
