prove INST_correct
simplify and strengthen termsem_INST

we don't need to assume the tyin only has variables in its domain.
attempt to prove INST_TYPE_correct, but looks false

or at least non-obvious: the problem is the term (constant) valuation
has changed and e.g. might not satisfy the axioms any more... need to
know that the change was benign, which I think means we need to
constrain term valuations more.