progress on proving the shol semantics is functional

reduced to a cheat in the case for the Tyabs constant introduced for a
type definition, because I need to know that if there's some type
instantiation that gives the predicate term the right type, then it only
needs to bind the type variables that actually appear in the predicate term.
perhaps i could bake this condition into the semantics and hope it
doesn't push this proof elsewhere...