IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
array shift wf121 1. T : Type
2. i : 3. j : {i...}
4. n : 5. m1 : {n...}
6. a2 : {n..m1}T 7. <n,m1,a2>.l = i & <n,m1,a2>.u = j 8. m : n+m = i+m & m1+m = j+m
By:
Unfolds [`array_ub`;`array_lb`] 7
THEN
Rewrite (DepthC (pi1_evalC ORELSEC pi2_evalC)) 7
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
}
T
n+m = i+m & m1+m = j+m
