Def tl(l) == Case of l; nil  nil ; h.t  t

is mentioned by

Thm* L1,L2:T List. null(L2)  L1  tl(L2)  L1  L2	[sublist_tl]
Thm* as:T List, x:T. 0<||as||  (x  tl(as))  (x  as)	[member_tl]
Thm* L:T List. 0<||L||  (L ~ [hd(L) / tl(L)])	[list_decomp]

In prior sections: list 1

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