1. T : Type
2. m : 
3. 0<m
4. L:T List. m-1<||L||  (nth_tl(m-1;L) ~ [L[(m-1)] / nth_tl(1+m-1;L)])
5. L : T List
6. m<||L||
7. 0<m
8. 0<1+m
  m-1<||tl(L)||

By:	Inst Thm* l:A List. ||l||1  ||tl(l)|| = ||l||-1   [T;L]

None

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html