A,X:Type, P:(A), y:A, f:(XA).
  (Replace values x s.t. P(x) by y in f)  XA

By:	Compute Replace values x s.t. P(x) by y in f * i.if P(f(i)) y else f(i) fi THEN UnivCD

1

1. A : Type 2. X : Type 3. P : A 4. y : A 5. f : XA   (i.if P(f(i)) y else f(i) fi)  XA

4 steps

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