Refactor shifting in contexts

[timsueberkrueb]

Currently, our typing context maintains De-Bruijn indices with respect to the current context. This means that we need to shift the whole context whenever we push or pop a telescope. Instead, we should consider inserting types as-is and only shift on-demand, i.e. when we lookup a type.