SKOLEM_CONV : conv
STRUCTURE
SYNOPSIS
Proves the existence of a Skolem function.
DESCRIPTION
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.
SEEALSO
HOL  Trindemossen-1