SKOLEM_CONV
Conv.SKOLEM_CONV : conv
Proves the existence of a Skolem function.
When applied to an argument of the form !x1...xn. ?y. P, the
conversion SKOLEM_CONV returns the theorem:
|- (!x1...xn. ?y. P) = (?y'. !x1...xn. P[y' x1 ... xn/y])
where y' is a primed variant of y not free in the input term.
Failure
SKOLEM_CONV tm fails if tm is not a term of the form
!x1...xn. ?y. P.