----------------------------------------------------------------------
LIST_MK_PEXISTS                                            (PairRules)
----------------------------------------------------------------------
LIST_MK_PEXISTS : (term list -> thm -> thm)

KEYWORDS
rule, quantifier, existential.

LIBRARY
pair

SYNOPSIS
Multiply existentially quantifies both sides of an equation using the given
pairs.

DESCRIBE
When applied to a list of terms {[p1;...;pn]}, where the {pi} are all
paired structures of variables, and a theorem {A |- t1 = t2},
the inference rule {LIST_MK_PEXISTS} existentially quantifies both sides
of the equation using the pairs given, none of the variables in the pairs
should be free in the assumption list.

                A |- t1 = t2
   --------------------------------------  LIST_MK_PEXISTS ["x1";...;"xn"]
    A |- (?x1...xn. t1) = (?x1...xn. t2)




FAILURE
Fails if any term in the list is not a paired structure of variables,
or if any variable is free in the assumption list,
or if the theorem is not equational.

SEEALSO
Drule.LIST_MK_EXISTS, PairRules.PEXISTS_EQ, PairRules.MK_PEXISTS.

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