poor attempt to speed up proof of bool_extends
work towards bool_has_bool_interpretation

probably want to change the treatment of term valuations and
inteprets_on_as so as to only ever deal with proper type valuations (and
stop fussing about with ARB).

also proved a few lemmas about the boolean signature and ok terms in it.