finish proof of add_constraints_thm

add two lemmas to help:
  subterms of a term_ok term are term_ok, and
  it's possible to extend a valuation to a larger signature