There is a primitive, but little used, operation for doing recursion on lists. It is not much used because we tend to use more general methods for defining Recursive Functions but this specific recursion operator has some historical and pedagogical value. Also, in some other type systems, general recursion is not expressible, and such structural recursion operations must be built in.

Case of X; nil b ; x.y, rec:vf(x;y;v) is the form of list recursion.

Case of nil; nil b ; x.y, rec:vf(x;y;v) * b

Case of a.as; nil b ; x.y, rec:vf(x;y;v)
*
f(a;as;Case of as; nil b ; x.y, rec:vf(x;y;v))

Notice that there is a third argument to the list-splitting case; the application of the recursive function on the tail is passed in through it.
Actually, our (Case of X; nil e ; x.yf(x,y)) operator is simply the special case of this recursion operator in which the recursion on the tail is ignored.