Theoretical Pearls Enumerators of lambda terms are reducing
Henk P Barendregt · Journal of Functional Programming · 1992
Abstract A closed λ-term E is called an enumerator if Here ⋀ 0 is the set of closed λ-terms,. is the set of natural numbers and the ⌜ n ⌝ are the Church's numerals λ fx . f n x . Such an E is called reducing if, moreover An ingenious recursion theoretic proof by Statman will be presented, showing that every enumerator is reducing. I do not know any direct proof.