IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
flip adjacent111 1. k : 2. k 3. k 4. x1 : k 5. y1 : k 6. y1-x1 = 0
L:(k-1) List. (x1, y1) = compose_flips(L)
By:
InstConcl [nil] THEN Unfold `compose_flips` 0 THEN Unfold `compose_list` 0
THEN
Reduce 0