1. r : 
2. 0<r
3. L:Top List. ||nth_tl(r-1;L)|| = if r-1<||L|| ||L||-(r-1) else 0 fi
4. L : Top List
5. 0<r
6. r<||L||
  ||nth_tl(r-1;tl(L))|| = ||L||-r  

By:	InstHyp [tl(L)] 3 THEN RWO Thm* l:A List. ||l||1  ||tl(l)|| = ||l||-1   -1 THEN MoveToConcl -1 THEN SplitOnConclITE

None

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