This post is a continuation of the previous blog post on proof automation for the data_encoding proofs.
data_encoding is a library used in the Tezos codebase to define binary and JSON encodings, by using some primitives and then combining these primitives with combinators.