mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
5Thm* f:(BA), x:B List, i,j:||x||. map(f;swap(x;i;j)) = swap(map(f;x);i;j)[map_swap]
cites the following:
3Thm* L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L||  [swap_length]
0Thm* f:(AB), as:A List. ||map(f;as)|| = ||as||  [map_length]
4Thm* L:T List, i,j,x:||L||. swap(L;i;j)[x] = L[((i, j)(x))][swap_select]
1Thm* f:(AB), as:A List, n:||as||. map(f;as)[n] = f(as[n])[map_select]
1Thm* a,b:T List. ||a|| = ||b||    (i:. i<||a||  a[i] = b[i])  a = b[list_extensionality]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb list 2 Sections MarkB generic Doc