mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
5Thm* L:T List, x:T, i,j:{1..(||L||+1)}.
Thm* swap([x / L];i;j) = [x / swap(L;i-1;j-1)]		[swap_cons]
cites the following:
1Thm* a,b:T List. ||a|| = ||b||    (i:. i<||a||  a[i] = b[i])  a = b[list_extensionality]
4Thm* L:T List, i,j,x:||L||. swap(L;i;j)[x] = L[((i, j)(x))][swap_select]
3Thm* L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L||  [swap_length]
0Thm* a:T, as:T List, i:. 0<i  i||as||  [a / as][i] = as[(i-1)][select_cons_tl]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb list 2 Sections MarkB generic Doc