'a:S, e:'a, f:('a'a).
  (fn1:('a). fn1(0) = e & (n:. fn1(n+1) = f(fn1(n),n)))
  & (fn1,y:('a).
  & (fn1(0) = e & (n:. fn1(n+1) = f(fn1(n),n))
  & (& y(0) = e
  & (& (n:. y(n+1) = f(y(n),n))
  & (
  & (fn1 = y)

None

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