Remove the usage of infix, overloaded syntax in why3 output

[xldenis]

This PR removes as much infix syntax as possible in the Why3 output. A few operators must be left: /\ \/, = and <> must be emitted as before since they have special handling down later in the compilation pipelines.

Several issues remain:

• Task views now talk about le1 instead of <=.
• Some proofs are not passing, most likely related to special encoding in smt of certain symbosl by drivers.
• The code is rather ugly.

[xldenis]

Oh additionally, the encoding of slice / array literals is broken since the [| ... |] syntax depends on their existing a (=) symbol which happens to have the correct type.

[xldenis]

This PR doesn't really advance us unless we also get rid of the coercions for the to_int function in machine integers, which we can do but requires more work and tedium.

Additionally, this has really clear performance implications, as why3 doesn't have good support for inlining so wrapping definitions can have huge impact even if those wrappers are trivial.

Perhaps this can be revived in a different form: making all arithmetic and comparison operators let functions or let predicates (as appropriate).