Move implementation of variant into holSyntaxExtraTheory

The motivation here is to make it easier to EVAL the inference system.
The definitions of INST and VSUBST call VARIANT which doesn't have an
EVAL-able definition. But the monadic functions included an
implementation of variant that is obviously evaluatable, and was proved
equivalent.

I have moved the definition of variant (and its dependencies) and its
relevant correctness proofs into holSyntaxExtraTheory, and used them to
provide alternative theorems for INST and VSUBST that will work better
with EVAL.

The theorem for INST is not perfect because it has a precondition
requiring the term argument to be welltyped (and thus cannot be used
directly with EVAL). However, in contexts where welltypedness is known,
it can be used to substitute calls to INST with calls to an alternative
function using the new equations (not defined in this commit).