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

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