various tweaks of definitions, and some progress on add_constraints_thm