Nuprl - mb_list_2 LEMMAs for swap

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

Rank	Theorem	Name
5	Thm* L1:T List, i,j:\|\|L1\|\|. swap(swap(L1;i;j);i;j) = L1	[swap_swap]
cites the following:
1	Thm* a,b:T List. \|\|a\|\| = \|\|b\|\| (i:. i<\|\|a\|\| a[i] = b[i]) a = b	[list_extensionality]
3	Thm* L:T List, i,j:\|\|L\|\|. \|\|swap(L;i;j)\|\| = \|\|L\|\|	[swap_length]
1	Thm* k:, x,y,i:k. (y, x)((y, x)(i)) = i	[flip_twice]
4	Thm* L:T List, i,j,x:\|\|L\|\|. swap(L;i;j)[x] = L[((i, j)(x))]	[swap_select]

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