(bad state) partial switch to using RDA's polymorphic values

also several lemmas about extending/reducing context, which motivated
this change. however, it seems like polymorphic values are probably a
mistake: we don't want term valuations to be general over type
valuations, since we actually always know what type valuation is
relevant. so, will probably go back to making being a term valuation
depend on a particular type valuation.

the other motivation for the change was to make type valuations
unconstrained on bad types (so a type valuation for an extended
signature is still a type valuation for any reduction of that signature:
it's allowed to send the undefined stuff anywhere). will keep this part
of the change.
revert polymorphic values, and prove new_const/new_type correct

these are the pure context updates that just add a new constant/type
operator to the context without defining them. essentially, have proved
that this is conservative.
prove new_axiom correct (after fixing it)

easy because we're concerned about validity of sequents in context:
we're allowed to assume all the axioms in the context hold, so adding a
new one doesn't make anything unproveable and lets you prove it too.

of course, we will also need at some point a result saying that certain
contexts actually do have models (e.g. if they only declare as axioms
the particular axioms we know how to prove are true)