1. T : Type
2. as : T List
3. x : T
4. 0<||as||
5. i : 
6. i<||tl(as)||
7. x = tl(as)[i]
  i:. i<||as|| & x = as[i]

By:	RWO Thm* l:A List. ||l||1  ||tl(l)|| = ||l||-1   -2 THEN InstConcl [i+1] THEN AllHyps (RWO Thm* as:A List, n:(||as||-1). tl(as)[n] = as[(n+1)])

None

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