I was looking at some slides of John Longley's here, 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, but not much else, other than that "Kierstead terms" have provided handy examples for certain notions of "safety" (see Example 1.5 here) or "innocence" (see section 2.3.1, here).

**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?*