Nuprl - mb_list_2 LEMMAs for flip

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

Rank	Theorem	Name
2	Thm* k:, x,y:k. L:(k-1) List. (x, y) = compose_flips(L)	[flip_adjacent]
cites the following:
1	Thm* k:, x,y,z:k. Thm* y = z x = y (x, y) = compose_list([(x, z); (y, z); (x, z)])	[flip_lemma]
1	Thm* k:, L1,L2:(k-1) List. Thm* compose_flips(L1) o compose_flips(L2) = compose_flips(L1 @ L2)	[compose_flips_append]
0	Thm* k:, i,j:k. (i, j) = (j, i)	[flip_symmetry]

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