specialisation

- type soundness proof finished
- semantic soundness proof still misses the case for accumulations