X_SKOLEM_CONV takes two arguments. The first is a variable f, which
must range over functions of the appropriate type, and the second is a term of
the form !x1...xn. ?y. P. Given these arguments, X_SKOLEM_CONV returns
which expresses the fact that a skolem function f of the
universally quantified variables x1...xn may be introduced in place of the
the existentially quantified value y.
|- (!x1...xn. ?y. P) = (?f. !x1...xn. tm[f x1 ... xn/y])