A

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.