bit more progress on add_constraints_thm

reduced to showing that the constrained interpretation still satisfies
the axioms in the original context.