Strong normalization

The declarative part now needs some equations which commute coerce and
type names, e.g., when can we exchange `coerce` and `pi`?