define subterms, and prove a tighter version of termsem_consts

it only cares about things that actually appear in the term (rather
than any valid term/type in the same signature).