Deskolemization, equality and logical complexity

Skolemization is a well-known method to eliminate one type of quantifier from formulas and (cut-free) proofs. We are interested in questions about proof complexity (in the sense of logical complexity, i.e. the number of sequents in a proof): how much shorter can a proof of the Skolemization of F be when compared to proofs of F? We will show that in the presence of the equality schema, there exists an arbitrary speed-up. The result is proved using techniques from the generalization of proofs.