Def  Y(f) == (x.f(x(x)))(x.f(x(x)))

is mentioned by

Def  Iter(f;u) i:{a..b}. e(i) Def  == if a<b f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1)) else u fi Def  (recursive)

[iter_via_intseg]

In prior sections: num thy 1

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