Translation: remove the "of_value" definitions

[clarus]

Context: for each new data type in the link phase, we need to define corresponding of_value_with and of_value. But the two are very similar.

The goal of this task is to remove of_value definitions. These are trying to infer the type of a Value.t in addition of finding the corresponding value in idiomatic Rocq. Thanks to the addition of more type annotations in the generated Rocq, these should not be needed anymore.

We can consider the task done once we can remove the OfValue.t definition.