+simply-typed lambda calculus. It can be expressed in System F,
+however. Here is one way, coded in
+[[Benjamin Pierce's type-checker and evaluator for
+System F|http://www.cis.upenn.edu/~bcpierce/tapl/index.html]] (the
+part you want is called "fullpoly"):
+
+ N = All X . (X->X)->X->X;
+ Pair = All X . (N -> N -> X) -> X;
+ let zero = lambda X . lambda s:X->X . lambda z:X. z in
+ let snd = lambda x:N . lambda y:N . y in
+ let pair = lambda x:N . lambda y:N . lambda X . lambda z:N->N->X . z x y in
+ let suc = lambda n:N . lambda X . lambda s:X->X . lambda z:X . s (n [X] s z) in
+ let shift = lambda p:Pair . p [Pair] (lambda a:N . lambda b:N . pair (suc a) a) in
+ let pre = lambda n:N . n [Pair] shift (pair zero zero) [N] snd in
+
+ pre (suc (suc (suc zero)));
+
+We've truncated the names of "suc(c)" and "pre(d)", since those are
+reserved words in Pierce's system. Note that in this code, there is
+no typographic distinction between ordinary lambda and type-level
+lambda, though the difference is encoded in whether the variables are
+lower case (for ordinary lambda) or upper case (for type-level
+lambda).
+
+The key to the extra flexibility provided by System F is that we can
+instantiate the `pair` function to return a number, as in the
+definition of `pre`, or we can instantiate it to return an ordered
+pair, as in the definition of the `shift` function. Because we don't
+have to choose a single type for all uses of the pair-building
+function, we aren't forced into a infinite regress of types.