Massive refactoring

- merged Ter and Exp
- uniformized treatment of primitive notions
and necessary renaming and refactoring