PEXISTS_TAC : (term -> tactic)
STRUCTURE
PairRules
LIBRARY
pair
SYNOPSIS
Reduces paired existentially quantified goal to one involving a specific witness.
DESCRIPTION
When applied to a term q and a goal ?p. t, the tactic PEXISTS_TAC reduces the goal to t[q/p]. 
    A ?- ?p. t
   =============  EXISTS_TAC "q"
    A ?- t[q/p]

FAILURE
Fails unless the goal’s conclusion is a paired existential quantification and the term supplied has the same type as the quantified pair in the goal.
EXAMPLE
The goal: 
   ?- ?(x,y). (x,y)=(1,2)
can be solved by: 
   PEXISTS_TAC "(1,2)" THEN REFL_TAC

SEEALSO
EXISTS_TAC, PEXISTS
HOL  Kananaskis-13