Possibly add in syntax for substitutions

[evinism]

As a teaching tool, I feel like substitutions are extremely necessary in order to understand the lambda calculus. This doesn't cover them at all.

We should make that not the case.