Better modularisation of the type-checker for expressions and proofs. Its usable in fun also.