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

is mentioned by

Def zip(as;bs) Def == Case of as Def == Canil  nil Def == Caa.as'  Case of bs; nil  nil ; b.bs'  [<a,b> / zip(as';bs')] Def (recursive)	[zip]
Def list_accum(x,a.f(x;a);y;l) Def == Case of l; nil  y ; b.l'  list_accum(x,a.f(x;a);f(y;b);l') Def (recursive)	[list_accum]

In prior sections: list 1 mb nat

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