merged

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)