Normal form: when we read back, we get a normal form expression.
Read back: read back functions, converting terms to normal forms with de-bruijn indices so we do not need to deal with alpha conversions.
Reduction: eval and eval's friends.
Syntax: term, expression, context.
Methods are defined in
Type checking: the four type checking functions --