1. A : Type
2. P : AAProp
3. a,b:A. P(a,b)  P(b,a)
4. a : A List
5. b : A List
6. i : (||a||-1)
7. P(a[i],a[(i+1)])
8. b = swap(a;i;i+1)
9. b[i] = a[(i+1)]
10. b[(i+1)] = a[i]
11. ||b|| = ||a||
12. a = swap(b;i;i+1)
13. x:||b||. x = i  x = i+1  b[x] = a[x]
  P(b[i],b[(i+1)])

None

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