Def compose_flips(L) == compose_list(map(i.(i, i+1);L))

is mentioned by

Thm* k:, p:(kk). Bij(k; k; p)  (L:(k-1) List. p = compose_flips(L))	[permute_by_flips]
Thm* k:, x,y:k. L:(k-1) List. (x, y) = compose_flips(L)	[flip_adjacent]
Thm* k:, L1,L2:(k-1) List. Thm* compose_flips(L1) o compose_flips(L2) = compose_flips(L1 @ L2)	[compose_flips_append]

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html