Thanks to #391 and #423, it is now fairly easy to remove coercions from Gospel type-checker

I have done so in this branch.
But this necessitate some heavy manual lifting in the specifications.
For the sake of example, I have updated the documentation to reflect a bit the amount of verbosity this generates.
I haven't updated the tests.

In principle, the manual lifting should be replaced by the use of models.
We don't want to write to_seq my_array, but rather give the type array a logical model of type sequence.
The problem is that the type array, and more importantly because it is the most used, the type int are defined in the standard library.
We can't just add specifications to the standard library, nor should we as Gospel definition is a moving target and its implementation still buggy.

What we could have is a re-exposition of (a subset of) OCaml standard library with Gospel annotations in the interface (at least logical models for the types).
Gospel type-checker would open this annotated standard library before type-checking a module, so that logical models are available.

This would also be a step forward a better separation between the programming world and the logical world, which is something we have been discussing.