PCHOOSE : term * thm -> thm -> thm
STRUCTURE
PairRules
LIBRARY
pair
SYNOPSIS
Eliminates paired existential quantification using deduction from a particular witness.
DESCRIPTION
When applied to a term-theorem pair (q,A1 |- ?p. s) and a second theorem of the form A2 u {s[q/p]} |- t, the inference rule PCHOOSE produces the theorem A1 u A2 |- t. 
    A1 |- ?p. s   A2 u {s[q/p]} |- t
   ------------------------------------  PCHOOSE ("q",(A1 |- ?q. s))
               A1 u A2 |- t
Where no variable in the paired variable structure q is free in A1, A2 or t.
FAILURE
Fails unless the terms and theorems correspond as indicated above; in particular q must have the same type as the pair existentially quantified over, and must not contain any variable free in A1, A2 or t.
SEEALSO
CHOOSE, PCHOOSE_TAC, PEXISTS, PEXISTS_TAC, PSELECT_ELIM
HOL  Kananaskis-14