Who Cites delete fenum value?
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)
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

Syntax:

Replace value k by f(m) in f

has structure:

delete_fenum_value(k; f; m)

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