Def l_interval(l;j;i) == mklist(i-j;x.l[(j+x)])

is mentioned by

Thm* l:T List, i:||l||, j:i. last(l_interval(l;j;i)) = l[(i-1)]	[last_l_interval]
Thm* l:T List, i:||l||, j:i. hd(l_interval(l;j;i)) = l[j]	[hd_l_interval]
Thm* l:T List, i:||l||, j:(i+1), x:(i-j). l_interval(l;j;i)[x] = l[(j+x)]	[select_l_interval]
Thm* l:T List, i:||l||, j:(i+1). ||l_interval(l;j;i)|| = i-j	[length_l_interval]

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