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

By:	RWO Thm* L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L||   0 THEN Reduce 0

None

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