IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
length segment1 1. T : Type
2. as : T List
3. i : {0...||as||}
4. j : {i...||as||}
||as[i..j]|| = j-i
By:
RWW "u:segment length_firstn length_nth_tl" 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
||as[i..j
]|| = j-i
