T:Type, L1:T List, i,j:||L1||. swap(swap(L1;i;j);i;j) = L1

By:	Auto THEN Inst Thm* L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L||   [T;L1;i;j] THEN Inst Thm* L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L||   [T;swap(L1;i;j);i;j] THEN BackThru Thm* a,b:T List. ||a|| = ||b||    (i:. i<||a||  a[i] = b[i])  a = b

1

1. T : Type 2. L1 : T List 3. i : ||L1|| 4. j : ||L1|| 5. ||swap(L1;i;j)|| = ||L1||   6. ||swap(swap(L1;i;j);i;j)|| = ||swap(L1;i;j)||   7. i1 :  8. i1<||swap(swap(L1;i;j);i;j)||   swap(swap(L1;i;j);i;j)[i1] = L1[i1]

1 step

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