Define NamedEnv directly instead of deriving it from Env

[skeuchel]

In the codebase we are using two kinds of environments. Env carries a piece of data for every element of a context, and NamedEnv carries data for every item in named context.

Named context are just contexts with bindings as elements and named environments are just environments after throwing away the name of a binding. Unfortunately, in this setup unification sometimes fails to figured out the type of data and requires manual annotation. This is especially cumbersome in proofs with rewrites failing because of this.

Only tuples currently make use of Env, which means overall we are using NamedEnv much more extensively than Env. I think it would make sense to provide a standalone definition of NamedEnvs, even if this means duplicating code. We probably need fewer lemmas for Env so it's not doubling that part of the framework. Alternatively, we can also use just NamedEnv and define the tuple-related machinery with unit as the type of names.