Fabrice Marchant wrote:
> After Coq, maybe could we program this in Lisp ?

Yes, although this is rather off-topic.  Here are two solutions in 
(rather rusty) Scheme, both zero-based again.  A curried version:

   (define (f n)
     (cond
      ((zero? n) (lambda (x) x))
      (#t        (lambda (_) (f (- n 1))))))

Now

   > ((f 0) 1)
   1
   > (((((f 3) 1) 2) 3) 4)
   4

An uncurried version:

   (define (f n)
     (lambda args (list-ref args n)))

Now

   > ((f 0) 1)
   1
   > ((f 3) 1 2 3 4)
   4

Jeremy.