'b,'a:S, x:'b, f:('b'a('a List)'b).
  (fn1:(('a List)'b). 
  (fn1(nil) = x & (h:'a, t:'a List. fn1(cons(h; t)) = f(fn1(t),h,t)))
  & (fn1,y:(('a List)'b).
  & (fn1(nil) = x & (h:'a, t:'a List. fn1(cons(h; t)) = f(fn1(t),h,t))
  & (& y(nil) = x
  & (& (h:'a, t:'a List. y(cons(h; t)) = f(y(t),h,t))
  & (
  & (fn1 = y)

None

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