Some results on extensionality in lambda calculus

In this paper we consider the problem (due to A. Cantini) of the existence of a λ -theory T such that: recursive enumerable; -rule holds in T (that is: if two terms M , N are such that for every closed term Q , M Q = N Q holds in T , then M = N holds in T ). ve affirmatively this problem. elated questions are also discussed.