...
Some equivalences we are not enforcing:
new x in \ { new y in \ { P \ } \ } is not the same as new y in \ { new x in \ { P \ } \ }
- Any commutativity of arithmetic expressions.
- Binding order of free variables in process patterns is not commutative.
...