partial reduction

- formalisation of reduction semantics with partial environments
- soundness proof

Missing: a function implementation of the reduction semantics. This
requires an implementation of finite mappings.