1. k : 
2. x : k
3. y : k
  L:(k-1) List. (x, y) = compose_flips(L)

By:	Assert (n:, x,y:k. y-x = n  (L:(k-1) List. (x, y) = compose_flips(L)))

1	n:, x,y:k. y-x = n  (L:(k-1) List. (x, y) = compose_flips(L))	17 steps
2	4. n:, x,y:k. y-x = n  (L:(k-1) List. (x, y) = compose_flips(L))   L:(k-1) List. (x, y) = compose_flips(L)	5 steps

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