Don't axiomatize operations
This defines an algebraic type to represent operations. This allows pattern-matching on the operations emitted by a contract which is required to integrate Mi-Cho-Coq with contract interaction frameworks such as ConCert. This is also related to https://gitlab.com/nomadic-labs/coquille/-/issues/5.