Add `let`-bindings to the context

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.