PSELECT_EQ : (term -> thm -> thm)
STRUCTURE
LIBRARY
pair
SYNOPSIS
Applies epsilon abstraction to both terms of an equation.
DESCRIPTION
When applied to a paired structure of variables p and a theorem whose conclusion is equational:
    A |- t1 = t2

the inference rule PSELECT_EQ returns the theorem:

    A |- (@p. t1) = (@p. t2)

provided no variable in p is free in the assumptions.

         A |- t1 = t2
   --------------------------  SELECT_EQ "p"      [where p is not free in A]
    A |- (@p. t1) = (@p. t2)

FAILURE
Fails if the conclusion of the theorem is not an equation, of if p is not a paired structure of variables, or if any variable in p is free in A.
SEEALSO
HOL  Kananaskis-14