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-14