Simplify how user-provided quantifier attributes are handled (#6963)

Simplify how user-provided quantifier attributes are handled (#6963)

This makes INST_ATTRIBUTE (optionally) take multiple children, giving a way for the user to set attributes on quantified formulas, which does not require a new API command.

This is a special case of term annotations that occur as the body of a quantified formula.

If we need to extend our API to support further user-provided attributes, we should use a similar approach, e.g. a new kind ANNOTATE.