Reversible coercion from choice_type

[MarkusKL]

(This should be redirected to main once #70 has been merged)
I do not intend this to be merged for now. I just want to show progress and discuss ideas and ramifications.

I have managed to make a reversible coercion from choice_type, which allows us to derive much more type information by unification. The following checks are valid and derive the appropriate type information. The checks fail without a reversible coercion.

Check ([fmap (true, false)] : _ : choice_type).
Check (nat * bool * list unit  : choice_type).

The changes this will allow are vast. It would allow us to:

• Remove lots of type annotations that are simply derived automatically.
• Remove some workarounds in the examples that are obsolete.
• Remove notation such as 'nat, 'map, \times, 'bool etc. to the benefit of the user.
• Optionally remove type annotations when defining a package.
• Simplify the automation (code_simpl, sync, swap), not least as I think tools like auto with hint databases is much more powerful now.
• Prepares for complete removal of inductive choice_type (which probably depends on polymorphic universes in Hierarchy Builder).

This should also fix some of the issues with using assert, as it is defined over choice_type. In contrast, raw_code is defined over choiceType which already has a reversible coercion through HB.

I had to make two changes to the existing code:

• Make all arguments explicit with @ in some uses of rreflexivity_rule. I am not sure why it is necessary and without the fix it only breaks deep within SigmaProtocol.v.
• In SymmRatched.v the lemma code_link_map_loop that was added to the simplification database actually works, so manual invocations can be removed.

[spitters]

Nice!

BTW we've discussed using Deriving, but I'm not sure we're actually doing this at the moment.
https://github.com/arthuraa/deriving?tab=readme-ov-file#predefined-instances