mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
2Thm* R:(TTProp), k:, x,y:T.
Thm* (x R^k y)
Thm* 
Thm* (L:T List. 
Thm* (||L|| = k+1   & L[0] = x & last(L) = y & (i:k. L[i] R L[(i+1)]))		[rel_exp_list]
cites the following:
1Thm* L:T List, x:T. null(L)  last([x / L]) = last(L)[last_cons]
0Thm* a:T, as:T List, i:. 0<i  i||as||  [a / as][i] = as[(i-1)][select_cons_tl]
1Thm* as:A List. as = nil  ||as||1[length_of_not_nil]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb list 2 Sections MarkB generic Doc