12Actually, epsilon-terms are special kind of Skolem functions; it is pointed out in [Monk, The Hilbert ε-operator, p. 481] and in [Mints, Sec. 2.: Quantifier-Free Extensions of Formulas and ε-Theorems)].