use lemma to simplify part of add_constraints_thm

still can't prove the whole thing though
change valid_constraints_def; add_constraints_thm follows

however the new valid_constraints_def might put too much burden on the
automation, since it needs to say the axioms are satisfied even when a
constraint is not given. i.e. i've just shifted this work elsewhere.