define INST, and attempt to prove INST_HAS_TYPE

The HOL Light proof of the latter is very long and difficult to read.
The HOL4 proof is currently riddled with cheats.