A,B:Type, f:(BA), x:B List, i,j:||x||.
  map(f;swap(x;i;j)) = swap(map(f;x);i;j)

By:

Auto THEN BackThru Thm* a,b:T List. ||a|| = ||b||    (i:. i<||a||  a[i] = b[i])  a = b THEN Try (RWO Thm* f:(AB), as:A List, n:||as||. map(f;as)[n] = f(as[n]) 0) THEN Try (RWO Thm* L:T List, i,j,x:||L||. swap(L;i;j)[x] = L[((i, j)(x))] 0) THEN Try (RWO Thm* f:(AB), as:A List, n:||as||. map(f;as)[n] = f(as[n]) 0) THEN All (RWO Thm* f:(AB), as:A List. ||map(f;as)|| = ||as||  ) THEN Try (RWO Thm* f:(AB), as:A List. ||map(f;as)|| = ||as||   0) THEN All (RWO Thm* L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L||  ) THEN Try (RWO Thm* f:(AB), as:A List. ||map(f;as)|| = ||as||   0)

None

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