Def  (Replace values x s.t. P(x) by y in f)(i) == if P(f(i)) y else f(i) fi

is mentioned by

Def  Replace value k by f(m) in f == Replace values x s.t. x=k by f(m) in f

[delete_fenum_value]

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