Type checker
Issue #5
new
Write a type checker which takes preterms and returns intrinsically typed terms and only checks equality of typed terms, hence our normalisation proof can be used.