Enumerators of lambda Terms are Reducing
A closed X-term E is called an enumerator if =j )M. Here A is the set of closed X-terms,. is the set of natural numbers and the r w~> are the Church's numerals Xfx.f"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.