P_PCHOOSE_TAC : (term -> thm_tactic)
STRUCTURE
PairRules
LIBRARY
pair
SYNOPSIS
Assumes a theorem, with existentially quantified pair replaced by a given witness.
DESCRIPTION
P_PCHOOSE_TAC expects a pair q and theorem with a paired existentially quantified conclusion. When applied to a goal, it adds a new assumption obtained by introducing the pair q as a witness for the pair p whose existence is asserted in the theorem. 
           A ?- t
   ===================  P_CHOOSE_TAC "q" (A1 |- ?p. u)
    A u {u[q/p]} ?- t         ("y" not free anywhere)

FAILURE
Fails if the theorem’s conclusion is not a paired existential quantification, or if the first argument is not a paired structure of variables. Failures may arise in the tactic-generating function. An invalid tactic is produced if the introduced variable is free in u or t, or if the theorem has any hypothesis which is not alpha-convertible to an assumption of the goal.
SEEALSO
X_CHOOSE_TAC, PCHOOSE, PCHOOSE_THEN, P_PCHOOSE_THEN
HOL  Kananaskis-14