beta-eta was too much, because it transformed SOME x. P x into Eps P, which caused problems later; reintroduced old proof based on Metis, since it was a good test for the Skolemizer