make term datatype in inference system match implementation

This enables re-use of both the :term and :type datatypes in the
implementation, rather than using translations (hol_ty, hol_tm, hol_def)
into almost isomorphic types.

The most invasive change is for Abs which now takes two terms rather
than a destroyed variable. The fact that the first term ought to be a
variable is encoded in the typing relation. Some theorems now have an
additional welltyped assumption, and various definitions have changed to
accommodate this change in the datatype.

In the implementation, the proofs are all updated for the removal of the
extra datatypes and translation functions.