PSELECT_RULE

PairRules.PSELECT_RULE : (thm -> thm)

Introduces a paired epsilon term in place of a paired existential quantifier.

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.

See also

Drule.SELECT_RULE, PairRules.PCHOOSE, PairRules.PSELECT_CONV, PairRules.PEXISTS_CONV, PairRules.PSELECT_ELIM, PairRules.PSELECT_INTRO