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
eq_int	Def  i=j == if i=j true ; false fi
	Thm*  i,j:. (i=j)
inject	Def  Inj(A; B; f) == a1,a2:A. f(a1) = f(a2)  B  a1 = a2
	Thm*  A,B:Type, f:(AB). Inj(A; B; f)  Prop
int_seg	Def  {i..j} == {k:| i  k < j }
	Thm*  m,n:. {m..n}  Type
nat	Def   == {i:| 0i }
	Thm*    Type
le	Def  AB == B<A
	Thm*  i,j:. (ij)  Prop
nequal	Def  a  b  T == a = b  T
	Thm*  A:Type, x,y:A. (x  y)  Prop
one_one_corr_2	Def  A ~ B == f:(AB), g:(BA). InvFuns(A;B;f;g)
	Thm*  A,B:Type. (A ~ B)  Prop
replace_fn_values	Def  (Replace values x s.t. P(x) by y in f)(i) == if P(f(i)) y else f(i) fi
	Thm*  A,X:Type, P:(A), y:A, f:(XA). Thm*  (Replace values x s.t. P(x) by y in f)  XA

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