mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def {i..j} == {k:| i  k < j }

is mentioned by

Thm* L1,L2:T List. L1  L2  (n:(||L2||+1). L1 = firstn(n;L2))[firstn_is_iseg]
Thm* L:T List, i,j:||L||. i<j  [L[i]; L[j]]  L[sublist_pair]
Thm* L:T List, i:||L||. (L[i]  L)[select_member]
Thm* n:, f:(nT), i:n. mklist(n;f)[i] = f(i)[mklist_select]
Thm* n:, f:(nT). ||mklist(n;f)|| = n  [mklist_length]
Thm* L:T List, P:(||L||Prop).
Thm* (x:||L||. Dec(P(x)))
Thm* 
Thm* (i,j:||L||. P(i)  i<j  P(j))
Thm* 
Thm* (L_1,L_2:T List. L = (L_1 @ L_2) & (i:||L||. P(i)  ||L_1||i))		[append_split2]
Def L1  L2
Def == f:(||L1||||L2||). 
Def == increasing(f;||L1||) & (j:||L1||. L1[j] = L2[(f(j))]  T)		[sublist]

In prior sections: int 1 bool 1 int 2 list 1 mb basic mb nat

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

mb list 1 Sections MarkB generic Doc