The beta-eta-theory of the lambda-calculus is Post-complete. Can additional rules be added to extend the beta-theory of the lambda-calculus to get confluent theories other than the beta-eta theory?
This question violated my own rule that questions should explain why the questioner cares.
It struck me one night, not long before this site went into private beta, that because extensionality and the principle of the excluded middle are related, the eta rule is some sort of extensionality rule, and there are intermediate logics between intuitionistic and classical logic, then it would be interesting if there was such a thing as "intermediate eta" theories.
If I has done so, it would have been obvious that Evgenij's answer raises an obvious problem in the way I'd formulated the question, rather than being what I was after.