1. T : Type
2. L : T List
3. i : (||L||-1)
4. a : T
5. b : T
6. f : 2||swap(L;i;i+1)||
7. increasing(f;2)
8. j:2. [a; b][j] = L[((i, i+1)(f(j)))]
9. ||swap(L;i;i+1)|| = ||L||
10. a = L[((i, i+1)(f(0)))]
11. b = L[((i, i+1)(f(1)))]
12. (i, i+1)  ||L||||L||
13. (i, i+1)(f(0))<(i, i+1)(f(1))
  L[((i, i+1)(f(0)))] = L[(i+1)] & L[((i, i+1)(f(1)))] = L[i]

By:	MoveToConcl -1 THEN Unfold `flip` 0 THEN Reduce 0 THEN AssertBY (f(0)<f(1)) (AllHyps ((h. ((FwdThru Thm* k:, f:(k). increasing(f;k)  (x,y:k. x<y  f(x)<f(y)) (([h] ((THEN ((BackThru -1)) THEN AutoBoolCase (f(0)=i) THEN AutoBoolCase (f(1)=i) THEN AutoBoolCase (f(0)=i+1) THEN AutoBoolCase (f(1)=i+1)

None

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