Implement shifting.
Collapse the shifting definition.
Implement substitution.
Shifting and substitution are in terms of `map`.
β-reduction substitution.
Some terms are values.