Specify the data-encoding library

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

The goal is to write the properties we have to prove on the data-encoding library, according to the description of the milestone https://gitlab.com/nomadic-labs/coq-tezos-of-ocaml/-/milestones/21#tab-issues