Retain backward compatibility for destructors

[rkunnema]

#461 turned some function symbols into destructors (see
https://github.com/tamarin-prover/tamarin-prover/blob/develop/lib/term/src/Term/Builtin/Signature.hs#L20). This changes the interpretation of existing theories, so it seems better to retain backward compatability and:

• [ ] rename modified builtins to NAME-destructor
• [ ] explain new built ins in manual
• [ ] explain destructior and what they do in pure MSR theories in src/004_cryptographic-messages.md

Note: a challenge will be the proper way to handle fst/1 and snd/1... maybe allow a builtin to overwrite them? Or would this be a case where we want the destructor theory to be the default?

[rsasse]

The existing operators and builtins (including fst/1 and snd/1) should keep their previously existing semantics, please. It would be ok if there was a pairs-destructor theory or similar, that makes them destructors.