Strips universal quantifiers and antecedents of implications,
modifies the conclusion, and reorders the antecedents
DESCRIPTION
REORDER_ANTS_MOD f g combines the effects of REORDER_ANTS_MOD f
and applies the function g to the ultimate consequent of the
theorem, as does underAIs.