add a data-type mechanism, desugaring to a Church-encoding

[meisl]

Consider using bit-strings (List Bool) for the type/ctor-tag. This would require to re-do ADT List with at least three-way mutual recursion (-> #33), but has the benefit of greatly simplifying the task of adding more ctors to an ADT.
It'd also open up an easy way of adding support for (runtime) type tags as well: instead a flat List Bool we'd use a List (List Bool), one determining the runtime type, another determining the ctor used, ....
We might even provide the actual fields of the ADT instance in a List (rather than as top-level args), thus making the interface for both, predicates and projections completely uniform.