IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
select append front1221 1. T : Type
2. T List
3. bs : T List
4. T 5. v : T List
6. i:||v||. (v @ bs)[i] = v[i]
7. i : (||v||+1)
8. i = 0
(v @ bs)[(i-1)] = v[(i-1)]
By:
BackThru 6
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
i:
||v||. (v @ bs)[i] = v[i]
i = 0
(v @ bs)[(i-1)] = v[(i-1)]
