manual proving of various hypotheses of an example löb hypothesis

the term uses only boolean constants and some type variables. reduced
the hypotheses down to is_set_theory, is_in, and things about the
interpretation and term valuation, i.e. removed things about the
signature and type valuation.