1. A : Type
2. P : AAProp
3. X : A List
4. Y : A List
5. a : A
6. b : A
7. P(a,b)
  (X @ [b; a / Y]) = swap(X @ [a; b / Y];||X||;||X||+1)

By:	BackThru Thm* a,b:T List. ||a|| = ||b||    (i:. i<||a||  a[i] = b[i])  a = b

1	||X @ [b; a / Y]|| = ||swap(X @ [a; b / Y];||X||;||X||+1)||	1 step
2	8. i :  9. i<||X @ [b; a / Y]||   (X @ [b; a / Y])[i] = swap(X @ [a; b / Y];||X||;||X||+1)[i]	17 steps

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