Some progress on building a direct unifier for types.

The HOL/examples unifier works on s-expressions, and the initial
inferencer relied on encoding/decoding ML types to/from unifier sexps,
which we don't want to (operationally) do at compile time (or
type-inference time).  So we are defining new constants in terms of the
unifier ones + encoding and decoding and then proving operational
equations about the new constants that should allow them to run without
the encodings, while at the same time allowing us to still use the
existing theorems about the unifier.