  There are several ways to formally represent families of data, such as lambda
terms, in a type theory such as the dependent type theory of Coq. Mathematical
representations are very compact ones and usually rely on the use of dependent
types, but they tend to be difficult to handle in practice. On the contrary,
implementations based on a larger (and simpler) data structure combined with a
restriction property are much easier to deal with.
  In this work, we study several families related to lambda terms, among which
Motzkin trees, seen as lambda term skeletons, closable Motzkin trees,
corresponding to closed lambda terms, and a parameterized family of open lambda
terms. For each of these families, we define two different representations,
show that they are isomorphic and provide tools to switch from one
representation to another. All these datatypes and their associated
transformations are implemented in the Coq proof assistant. Furthermore we
implement random generators for each representation, using the QuickChick
plugin.
