Verify all the missing compare functions
Requires https://gitlab.com/nomadic-labs/coq-tezos-of-ocaml/-/issues/78
The goal of this issue is to exhaustively verify all the compare functions of the protocol. The list can be obtained from the previous issue https://gitlab.com/nomadic-labs/coq-tezos-of-ocaml/-/issues/78 This task should be done at the end of the milestone and is mainly a cleaning task, to verify the compare functions we missing in other tasks. Most of the missing compare functions should be trivial ones (aliases). In this case, it is possible to directly call the automated tactic, without doing an equality proof. There may be new complex compare functions added into the protocol, as the code keeps evolving.