WIP: Subject reduction for the base + toplevel fragment

We want to prove that evaluation preserves typing. This focuses on the base fragment that defines records. The toplevel fragment seems also required as it is deeply wired into the compiler architechture. It does not add complexity.

Most of the complexity of the proof comes from the Ott treatment of n-ary constructions which are unfortunately ubiquitous in the base fragment.