bit more progress on add_constraints_thm

but looks like I might need either to weaken the statement or to prove
something stronger about how the term semantics depends on the
interpretation. currently it says you can change interpretation as long
as the new one agrees on the signature; but it may need to say that you
can change it as long as it agrees on the constants actually appearing
in the term.