'a:S, P:(('a List)), n:.
  (l:'a List. ||l|| = n+1    P(l))
  
  (l:'a List. ||l|| = n    (x:'a. P(cons(x; l))))

None

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