work on (manual) proving hypotheses

down to is_set_theory, is_in, and things about the the term valuation
(for free term variables).