more work on semantics_VSUBST, not obviously making progress
suggestions/comments on semantics after chat with Scott
WIP: use finite map for type valuation

as with the term valuation, it is perhaps nicer to be explicit about the
domain of the variables the semantics is dealing with: in particular,
when we want to get the semantics of a term that should have no type
variables, it's nice to pass FEMPTY rather than a junky total function.
it may also be very helpful in making the correct precise statement when
it comes to doing the semantics of type and term substitution..

have changed the definition and started updating the proofs. commented
out most of the file since this breaks a lot of stuff early on.