Making Sense of Lambda Calculus 0: Abstration, Reduction, Substitution?

A nice way to think about eta-reduction is that it asserts something about the types of expressions in lambda calculus, namely that every expression is in fact a function.

If an expression M can appear in the left position of the function application operation, this implies that M is a function.

By way of analogy, if I have a formula x == x+0, this implies that x is a number.

Or, s == s + '' would imply that s is a string.

So, if M == lambda x. M(x), this is saying that M is a function.

> What follows the lambda is the list of arguments.

It would be clearer to say that what follows the lambda is the name of its (single) argument, not a list. And then explain that for notational convenience, you could abbreviate successive abstractions. Btw, if you really base it on lists, then do you allow an empty list as well?