Def {i..j} == {k:| i  k < j }

is mentioned by

Thm* n:, f:(nT), i:n. (f{n})[i] = f(i)	[select_listify_id]
Thm* as:T List. (i:||as||. as[i]){||as||} = as	[listify_select_id]
Thm* m,n:, f:({m..n}T). n<m  ||f{m..n}|| = n-m	[listify_length]
Thm* T:Type, m,n:, f:({m..n}T). f{m..n}  T List	[listify_wf]
Thm* f:(AB), as:A List, n:||as||. map(f;as)[n] = f(as[n])	[map_select]
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:A List, n:(||as||-1). tl(as)[n] = as[(n+1)]	[select_tl]
Thm* as,bs:T List, i:||as||. (as @ bs)[i] = as[i]	[select_append_front]
Thm* as,bs:T List, i:{||as||..(||as||+||bs||)}. (as @ bs)[i] = bs[(i-||as||)]	[select_append_back]

In prior sections: int 1 bool 1 int 2

Try larger context: StandardLIB IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html