fix holConsistencyTheory for recent changes to is_term_valuation
finish proof of bool_has_bool_interpretation

this means the definitions of the boolean operations are correct (they
constrain interpretations to interpret them with the desired semantics).
this will be important when showing the axiom of infinity (which depends
on many of these constants) is consistent.