Unification of Quantified Formulas

[Heizmann]

Sometimes I have terms of the following form

(and
    (exists ((x1 Int)) (= (select a x1) 0)
    (exists ((x2 Int)) (= (select a x2) 0)
    ....
    (exists ((x99 Int)) (= (select a x99) 0)
)

Obviously all conjunct are equivalent. I would like to detect this (not urgent). I there some code in Ultimate/SMTInterpol that approaches this problem? How is this problem called in the literature?

[danieldietsch]

The only thing that comes to mind is (re)naming quantified variables according to some scheme. One issue there is readability vs. already used variable names, but I think you know how to solve this. I do not know of any literature, perhaps @jhoenicke knows something.

[maul-esel]

If this is still an issue, something like Hashing Modulo Alpha-Equivalence might help.