thoughts on a converse to semantics_simple_inst

the semantics for a defined type could equally have been given by first
taking the semantics of all the arguments, then taking the subset of the
relevant term after extending the type valuation. (we instead do type
instantation on the term, then take the semantics in the original type
valuation.) it would be nice to have a theorem that justifies the
intuition that either approach is fine. semantics_simple_inst goes
halfway (only one direction). the other advantage of going the other way
is that it might make it easier to prove a type deconstruction rule sound.