Some definitions of interest.
delete_fenum_value	Def  Replace value k by f(m) in f == Replace values x s.t. x=k by f(m) in f
	Thm*  Inj({k:| P(k) }; {k:| Q(k) }; f) Thm*   Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }. Thm*  ((Replace value k by f(m) in f) Thm*  ( {u:| P(u) & u = m }{v:| Q(v) & v = k })
	Thm*  Inj((m+1); (k+1); f)  (Replace value k by f(m) in f)  mk
list_to_function	Def  seq:l(i) == l[i]
	Thm*  l:A List. seq:l  ||l||A
listify	Def  f{m..n} == if nm nil else f(m).f{(m+1)..n} fi  (recursive)
	Thm*  T:Type, m,n:, f:({m..n}T). f{m..n}  T List
le_int	Def  ij == j<i
	Thm*  i,j:. (ij)
length	Def  ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (recursive)
	Thm*  A:Type, l:A List. ||l||
	Thm*  ||nil||
let	Def  let x = a in b(x) == (x.b(x))(a)
	Thm*  A,B:Type, a:A, b:(AB). let x = a in b(x)  B

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html