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

is mentioned by

Def  n^k == if k=0 1 else n(n^(k-1)) fi  (recursive)	[exponentiation]
Def  HanoiSTD(n disks; from: p; to: q; indexing from: a) Def  == if n=0 <a,x,i. whatever> Def  == else HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a) Def  == else /m,s1. Def  == else HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m Def  == else HanoiSTD(+1) Def  == else /z,s2. <z,HanoiHelper(n; s1; i.p; s2; i.q)/r1,r2. r1 @(m) r2> fi Def  (recursive)	[hanoi_sol2_ala_generalPROG]

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