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

is mentioned

In prior sections: DiscreteMath

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