Implement type checker and type normalizer

[jaccokrijnen]

Currently we only have these in relation form, and our semantics preservation assumes we have a well-typed pre-term.