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

is mentioned by

Def t_iterate(l;n;t) Def == Case(t) Def == Case x;y => Def == Casen(t_iterate(l;n;x),t_iterate(l;n;y)) Def == Case tree_leaf(x) => Def == Casel(x) Def == Default => True Def (recursive)

[t_iterate]

In prior sections: prog 1

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