Prove INST_CORE_HAS_TYPE

In under half as many lines as the HOL Light version.

Key lemma I was missing was VARIANT_THM, which I hadn't realised was
necessary until looking at the HOL Light version more closely.