Currently the typing rule for let-bindings is rather weak, because the typing of the body cannot make use of the value of the let-bound variable. To make the typing of let-bindings work like it does in Agda, we'd need to have a separate entry for let-bound variables in the context that includes the value.