Update: remove unused existential variables

In this MR, we change the output of coq-of-ocaml so that existential variables which are not in use are not added to the cast_exists casts. This helps to infer the values for the existential types, as only one answer is generally possible. This also reduces slightly the verbosity of the code, eliminating dead code.

As an example, we complete the proof of dep_cost_of_instr_eq https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/proofs/script_interpreter_defs#dep_cost_of_instr_eq. Here there is some documentation about eliminating the casts: https://gitlab.com/foobar-land/roadmap-coq-tezos-of-ocaml/-/wikis/home#eliminate-cast-and-cast_exists

Finally, doing this proof we discovered some differences between the simulation and the actual code and fixed them (most are due to new code updates).