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)
  if P(L[n],L[(n+1)]) -1 else 0 fi+if P(L[(n+1)],L[n]) 1 else 0 fi
  =
  if ((n=n)(n+1=n+1))(P(L[n],L[(n+1)])) -1
  i; ((n=n+1)(n+1=n))(P(L[n],L[(n+1)])) 1
  else 0 fi+if ((n+1=n)(n=n+1))(P(L[(n+1)],L[n])) -1
  else 0 fi+i; ((n+1=n+1)(n=n))(P(L[(n+1)],L[n])) 1
  else 0 fi+else 0 fi

By:	AutoBoolCase (n=n) THEN AutoBoolCase (n=n+1) THEN AutoBoolCase (n+1=n) THEN AutoBoolCase (n+1=n+1)

None

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