use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.

further lower penalty associated with existentials in Sledgehammer's relevance filter, so that "exhaust" facts are picked up