For another example, the conjecture \A x (f(x) = 0) can be proved from the subgoal f(c) = 0, where c is a Skolem constant. As long as c is new, the proof is sound.
When an existential quantifier is being eliminated from a fact that contains free variables, or when the existential quantifier occurs in the scope of a universal quantifier, the quantified variable must be replaced by a term involving a Skolem function applied to the free and universally quantified variables. For example, the fact \A x (x < bigger(x)) can be obtained by eliminating the existential quantifier from \A x \E y (x < y) and replacing y by bigger(x). See the fix command and the generalization proof method.