A new version of the internal representation: we merge the former list
of variables and the split trees.

In the end, the split tree list can be seen as a term with holes: we
could go one step forward and drop this notion altogether, and
represent the split trees as regular coq terms.
Final commit on this branch (cleaning)