prove termsem_VSUBST and termsem_INST

the (proved) statement of the latter looks a bit worrying since it wants
to change to an interpretation of constants that ignores the type
valuation given to it...