1. A : Type
2. B : Type
3. P : AAProp
4. f : BA
5. x : B List
6. y : B List
7. i : (||x||-1)
8. P(f(x[i]),f(x[(i+1)]))
9. y = swap(x;i;i+1)
10. ||map(f;x)|| = ||x||
  map(f;y) = swap(map(f;x);i;i+1)

By:	HypSubst -2 0 THEN RWO Thm* f:(BA), x:B List, i,j:||x||. map(f;swap(x;i;j)) = swap(map(f;x);i;j) 0

None

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