trying to prove has_meaning_dbComb

lots of fiddly details trying to show that you can extend the
environment and valuations to cover the free variables in a term - the
details are because we want the extensions to preserve qualities like
only mentioning good types and typesets.
prove closing_envs_exist and work on has_meaning_dbComb