Def compose_list(L) == reduce(p,q. p o q;x.x;L)

is mentioned by

Thm* k:, x,y,z:k. Thm* y = z  x = y  (x, y) = compose_list([(x, z); (y, z); (x, z)])	[flip_lemma]
Thm* L1,L2:(TT) List. Thm* compose_list(L1) o compose_list(L2) = compose_list(L1 @ L2)	[compose_append]
Def compose_flips(L) == compose_list(map(i.(i, i+1);L))	[compose_flips]

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