1. T : Type
2. L : T List
3. P : TT
4. n : (||L||-1)
5. (n, n+1)  ||L||||L||
6. ||swap(L;n;n+1)|| = ||L||
7. f : ||L||||L||
8. i:||L||. f(i) = (n, n+1)(i)
  sum(if (i<j)P(swap(L;n;n+1)[i],swap(L;n;n+1)[j]) 1
  sum(else 0 fi | i < ||L||; j < ||L||)
  =
  sum(if (f(i)<f(j))P(swap(L;n;n+1)[(f(i))],swap(L;n;n+1)[(f(j))]) 1
  sum(else 0 fi | i < ||L||; j < ||L||)

By:	Assert Bij(||L||; ||L||; f)

1	Bij(||L||; ||L||; f)	3 steps
2	9. Bij(||L||; ||L||; f)   sum(if (i<j)P(swap(L;n;n+1)[i],swap(L;n;n+1)[j]) 1   sum(else 0 fi | i < ||L||; j < ||L||)   =   sum(if (f(i)<f(j))P(swap(L;n;n+1)[(f(i))],swap(L;n;n+1)[(f(j))]) 1   sum(else 0 fi | i < ||L||; j < ||L||)	1 step

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