PEXISTS_RULE : (thm -> thm)
STRUCTURE
LIBRARY
pair
SYNOPSIS
Introduces a paired existential quantification in place of a paired choice.
DESCRIPTION
The inference rule PEXISTS_RULE expects a theorem asserting that (@p. t) denotes a pair for which t holds. The equivalent assertion that there exists a p for which t holds is returned.
    A |- t[(@p. t)/p]
   ------------------  PEXISTS_RULE
       A |- ?p. t

FAILURE
Fails if applied to a theorem the conclusion of which is not of the form (t[(@p.t)/p]).
SEEALSO
HOL  Kananaskis-13