(proof-new) More features for SMT proof post-processor (#5246)

(proof-new) More features for SMT proof post-processor (#5246)

This updates the SMT proof postprocessor with additional stats. It also adds the feature to handle conjunctions as substitution, e.g. a child proof concluding (and (= x t) (= y s)) is interpreted as a substitution for x, y, whereas previously we insisted they must be provided separately.