Def {i...j} == {k:| ik & kj }

is mentioned by

Thm* as:T List, n:{0...||as||}, i:n. firstn(n;as)[i] = as[i]	[select_firstn]
Thm* as:T List, n:{0...||as||}, i:(||as||-n). nth_tl(n;as)[i] = as[(i+n)]	[select_nth_tl]
Thm* as:T List, i:{0...||as||}, j:{i...||as||}. ||as[i..j]|| = j-i	[length_segment]
Thm* as:A List, n:{0...||as||}. ||firstn(n;as)|| = n	[length_firstn]
Thm* as:A List, n:{0...||as||}. ||nth_tl(n;as)|| = ||as||-n	[length_nth_tl]

In prior sections: int 1

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html