Sync the data-encoding spec of the environment to the library

This is a follow-up of https://gitlab.com/nomadic-labs/coq-tezos-of-ocaml/-/issues/68

The goal is to connect our proofs and specifications to the file https://gitlab.com/nomadic-labs/coq-tezos-of-ocaml/-/blob/master/src/Proto_alpha/Environment/Proofs/Data_encoding.v where the axioms are written by hand. This might include updating the protocol proofs for the uses of data-encoding (although this can be done by creating separate tasks).

Since the protocol uses both the binary and JSON encodings, and since we only verify the JSON encoding, we should consider that the specification for the binary format is the same as the specification for the JSON format.