bit of work on INST_TYPE_correct

this proof is very annoyingly fiddly, and probably structured wrong..