IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
length nth tl22 1. A : Type
2. A List
3. A 4. v : A List
5. n:{0...||v||}. ||nth_tl(n;v)|| = ||v||-n 6. n : {0...||v||+1}
7. 0<n ||nth_tl(n-1;v)|| = ||v||+1-n
By:
RWO "5" 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
n:{0...||v||}. ||nth_tl(n;v)|| = ||v||-n
||nth_tl(n-1;v)|| = ||v||+1-n
