IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
select cons tl111 1. T : Type
2. a : T 3. as : T List
4. i : 5. 0<i 6. i||as||
7. 0<i hd(nth_tl(i-1;tl((a.as)))) = as[(i-1)]
By:
AbReduce 0 THEN Fold `select` 0
Generated subgoal:
1
as[(i-1)] = as[(i-1)]
Auto
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
||as||
hd(nth_tl(i-1;tl((a.as)))) = as[(i-1)]
