Def  == {i:| 0i }

is mentioned by

Thm* f:((T List)), t,t':. Thm* t<t'  concat(map(f;upto(t))) @ (f(t))  concat(map(f;upto(t')))	[concat_map_upto]
Thm* n,m:. firstn(n;upto(m)) ~ if nm upto(n) else upto(m) fi	[firstn_upto]
Thm* f:(TopTop), n:, l:Top List. firstn(n;map(f;l)) ~ map(f;firstn(n;l))	[firstn_map]
Thm* t',m:, T:Type, f:(T), P:(T). Thm* m+1||filter(P;map(f;upto(t')))|| Thm*  Thm* (t:. P(f(t)) & ||filter(P;map(f;upto(t)))|| = m  )	[filter_map_upto2]
Thm* i,j:. Thm* i<j Thm*  Thm* (f:(T), P:(T). Thm* (P(f(i))  ||filter(P;map(f;upto(i)))||<||filter(P;map(f;upto(j)))||)	[filter_map_upto]
Thm* n:, x,y:n. x before y  upto(n)  x<y	[before-upto]
Thm* n,i:. i<n  (i  upto(n))	[member_upto2]
Thm* n,i:. (i  upto(n))  i<n	[member_upto]
Thm* m:, n:m. upto(m)[n] = n	[select_upto]
Thm* i,j:. ij  upto(i)  upto(j)	[upto_iseg]
Thm* m:, n:(m+1). upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n)))	[upto_decomp]
Thm* n:. ||upto(n)|| ~ n	[length_upto]
Thm* n:. upto(n)  n List	[upto_wf]
Thm* f:(). (n:. f(n))  f(mu(f)) & (i:. i<mu(f)  f(i))	[mu-property]
Thm* f:(). (n:. f(n))  mu(f)	[mu_wf]
Thm* r:, L:Top List. ||nth_tl(r;L)|| = if r<||L|| ||L||-r else 0 fi	[general_length_nth_tl]
Thm* n,m:, f,i:Top. (f^n+m(i)) ~ (f^n(f^m(i)))	[fun_exp_add_sq]
Def IdLnk == IdId	[IdLnk]
Def Id == Atom	[Id]
Def finite-type(T) == n:, f:(nT). Surj(n; T; f)	[finite-type]

In prior sections: int 1 bool 1 int 2 list 1 sqequal 1 mb nat mb list 1 num thy 1 mb list 2

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