+This does take us beyond our (first-order) fragment of arithmetic, at least if we allow the bodies and arguments of λ-expressions to be any expressible value, including other λ-expressions. But we're having too much fun, so why should we hold back?
+
+So now we have a new kind of value our language can work with, alongside numbers and booleans. We now have function values, too. We can bind these function values to variables just like other values:
+
+`let id be` λ `x. x; y be id 5 in y`
+
+will evaluate to `5`. In reaching that result, the variable `id` was temporarily bound to the identity function, that expects an argument, binds it to the variable `x`, and then returns the result of evaluating `x` under that binding.
+
+This is what is going on, behind the scenes, with all the expressions like `succ` and `+` that I said could really be understood as variables. They have just been pre-bound to certain agreed-upon functions rather than others.
+
+
+### Containers ###
+
+*More coming*
+
+### Patterns ###
+
+*More coming*
+
+### Recursive let ###
+
+*More coming*
+
+### Comparing recursive-style and iterative-style definitions ###
+
+*More coming*
+
+