- 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 "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";