I was looking at some slides of John Longley's [here](http://homepages.inf.ed.ac.uk/jrl/Research/nsp-talk.pdf), where he mentions "the Kierstead functional"


$$\lambda f.f(\lambda x.f(\lambda y.x)) \ ,$$


(where $f$ should be of type $2$, and $x,y$ of ground type, so a functional of type $3$).


After ten or fifteen minutes of googling around I could only find that [this must be the Kierstead in question](https://math.la.asu.edu/~halk/), but not much else, other than that "Kierstead terms" have provided handy examples for certain notions of "safety" (see [Example 1.5 here](http://arxiv.org/pdf/0901.2399.pdf)) or "innocence" (see [section 2.3.1, here](http://hal.archives-ouvertes.fr/docs/00/15/03/55/PDF/galop06.pdf)).


**My questions**: *What is the origin of these lambda terms, that is, to which work of Kierstead can they be traced back? Are there other examples of their use in the literature?*



Background for Kierstead terms
This example (or a very similar one) first appeared in the literature in Kleene's paper 'Recursive functionals and quantifiers of finite types revisited I' (Proc. Generalized Recursion Theory II, Oslo) in 1978. Here Kleene attributes the example to his student Kierstead.


