first class functions with eager substitution
remove with from language definition

now implemented as a special case of function definition and application

(Exercise 6.3.1)