PFORALL_EQ : (term -> thm -> thm)
STRUCTURE
PairRules
LIBRARY
pair
SYNOPSIS
Universally quantifies both sides of an equational theorem.
DESCRIPTION
When applied to a paired structure of variables p and a theorem 
    A |- t1 = t2

whose conclusion is an equation between boolean terms: 

    PFORALL_EQ

returns the theorem: 

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

unless any of the variables in p is free in any of the assumptions. 

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

FAILURE
Fails if the theorem is not an equation between boolean terms, or if the supplied term is not a paired structure of variables, or if any of the variables in the supplied pair is free in any of the assumptions.
SEEALSO
FORALL_EQ, PEXISTS_EQ, PSELECT_EQ
HOL  Trindemossen-1