fixed trigger inference: testing if a theorem already has a trigger was too strict; fixed monomorphization with respect to triggers (which might occur schematically)

fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)

the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils

facilitate debugging