Push quantifications down seems like a smart move in most cases

[Broes De Cat]

Without pushing quantifications down, the same subformula can be grounded a lot of times where once would have been enough. For explicit quantifications, the user can solve this, but for for example functions, it is less obvious: ?x: P(a,x) is rewritten into ?x: !y: a=y => P(y,x) while a does not depend on x.