Nuprl - mb_list_2 LEMMAs for swap_adjacent

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

Rank	Theorem	Name
6	Thm* P:(AAProp), f:(BA), x,y:B List. Thm* (x swap adjacent[P(f(x),f(y))] y) Thm* Thm* (map(f;x) swap adjacent[P(x,y)] map(f;y))	[swap_adjacent_map]
cites the following:
1	Thm* f:(AB), as:A List, n:\|\|as\|\|. map(f;as)[n] = f(as[n])	[map_select]
0	Thm* f:(AB), as:A List. \|\|map(f;as)\|\| = \|\|as\|\|	[map_length]
5	Thm* f:(BA), x:B List, i,j:\|\|x\|\|. map(f;swap(x;i;j)) = swap(map(f;x);i;j)	[map_swap]

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