- Datatype package now also supports arbitrarily branching datatypes
(using function types).
- Added new simplification procedure for proving distinctness of
constructors.
- dtK is now a reference.
Goal "!vs. exec s vs (xs@ys) = exec s (exec s vs xs) ys";