Apply alpha equivalence to annotated quantified formulas (#5324)

Apply alpha equivalence to annotated quantified formulas (#5324)

Previously, alpha equivalence was not applied to quantified formulas with attributes, likely motivated by keeping alpha equivalent quantified formulas with different user patterns. It's not clear this is a good a idea. Moreover, this also implies that quantified formulas with user-provided names (which happens in e.g. Boogie benchmarks) also do not have alpha equivalence applied.

This makes it so that we apply alpha equivalence regardless of annotations.

FYI @barrettcw