Fixed: grounding of quantifiers.

The mistake was to precompute the H+ and then substitute all members of
H+ for all quantifiers. That should be incorrect (because of different
meaning of (A x. E y. phi) and (E y. A x. phi).

The new way is to add a new standard name for each quantifier. That
procedure implicitly brings the formula in prenex form.