PEXISTS_RULE

PairRules.PEXISTS_RULE : (thm -> thm)

Introduces a paired existential quantification in place of a paired choice.

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]).

See also

PairRules.PEXISTS_CONV, PairRules.PSELECT_RULE, PairRules.PSELECT_CONV, PairRules.PSELECT_INTRO, PairRules.PSELECT_ELIM