1. A : Type
2. L : A List
3. 1<||L||
4. ||tl(tl(L))|| = ||L||-2
5. i : 
6. i<||L||
7. i = 0
  L[i] = [L[0]; L[1] / tl(tl(L))][i]

By:	RWO Thm* a:T, as:T List, i:. 0<i  i||as||  [a / as][i] = as[(i-1)] 0 THENA Reduce 0

1

L[i] = [L[1] / tl(tl(L))][(i-1)]

5 steps

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