PSELECT_RULE : (thm -> thm)
STRUCTURE
LIBRARY
pair
SYNOPSIS
Introduces a paired epsilon term in place of a paired existential quantifier.
DESCRIPTION
The inference rule PSELECT_RULE expects a theorem asserting the existence of a pair p such that t holds. The equivalent assertion that the epsilon term @p.t denotes a pair p for which t holds is returned as a theorem.
       A |- ?p. t
   ------------------  PSELECT_RULE
    A |- t[(@p.t)/p]

FAILURE
Fails if applied to a theorem the conclusion of which is not a paired existential quantifier.
SEEALSO
HOL  Trindemossen-1