----------------------------------------------------------------------
PCHOOSE_THEN                                               (PairRules)
----------------------------------------------------------------------
PCHOOSE_THEN : thm_tactical

KEYWORDS
theorem-tactic, existential.

LIBRARY
pair

SYNOPSIS
Applies a tactic generated from the body of paired existentially quantified
theorem.

DESCRIBE
When applied to a theorem-tactic {ttac}, a paired existentially quantified
theorem:

    A' |- ?p. t


and a goal, {CHOOSE_THEN} applies the tactic {ttac (t[p'/p] |- t[p'/p])} to
the goal, where {p'} is a variant of the pair {p} chosen to have no
components free in the assumption list of the goal. Thus if:

    A ?- s1
   =========  ttac (t[q'/q] |- t[q'/q])
    B ?- s2

then

    A ?- s1
   ==========  CHOOSE_THEN ttac (A' |- ?q. t)
    B ?- s2

This is invalid unless {A'} is a subset of {A}.

FAILURE
Fails unless the given theorem is a paired existential quantification,
or if the resulting tactic fails when applied to the goal.

SEEALSO
Thm_cont.CHOOSE_THEN, PairRules.PCHOOSE_TAC, PairRules.P_PCHOOSE_THEN.

----------------------------------------------------------------------