Customise attributes pushed through introduction transformation

The transformation introduce_premises currently preserves only the attributes @expl: and @hyp_name:, i.e. when putting a variable binding into the context, only these attributes are pushed to the bound term. Other attributes are lost.

With this change, more attributes that should be pushed through variable bindings can be registered using Introduction.push_attributes_with_prefix.

This is necessary to preserve the VC attributes in SPARK when using split_vc (which uses introduce_premises) during counterexample generation.

The transformation generalize_introduced previously "un-pushed" only explanation attributes, and this change also includes hypothesis name attributes and other attributes that have been registered using Introduction.push_attributes_with_prefix.