PSELECT_CONV : conv
STRUCTURE
LIBRARY
pair
SYNOPSIS
Eliminates a paired epsilon term by introducing an existential quantifier.
DESCRIPTION
The conversion PSELECT_CONV expects a boolean term of the form "t[@p.t[p]/p]", which asserts that the epsilon term @p.t[p] denotes a pair, p say, for which t[p] holds. This assertion is equivalent to saying that there exists such a pair, and PSELECT_CONV applied to a term of this form returns the theorem |- t[@p.t[p]/p] = ?p. t[p].
FAILURE
Fails if applied to a term that is not of the form "p[@p.t[p]/p]".
SEEALSO
HOL  Kananaskis-14