Nuprl - mb_list_2 LEMMAs for symmetric_swap

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

Rank	Theorem	Name
7	Thm* P:(AAProp). Thm* (Sym x,y:A. P(x,y)) (Sym L1,L2:A List. L1 swap adjacent[P(x,y)] L2)	[symmetric_swap_adjacent]
cites the following:
6	Thm* L1,L2:T List, i,j:\|\|L1\|\|. Thm* L2 = swap(L1;i;j) Thm* Thm* L2[i] = L1[j] & L2[j] = L1[i] & \|\|L2\|\| = \|\|L1\|\| & L1 = swap(L2;i;j) Thm* & (x:\|\|L2\|\|. x = i x = j L2[x] = L1[x])	[swapped_select]

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