FORALL_EQ : (term -> thm -> thm)
STRUCTURE
Drule
SYNOPSIS
Universally quantifies both sides of an equational theorem.
DESCRIPTION
When applied to a variable x and a theorem A |- t1 = t2, whose conclusion is an equation between boolean terms, FORALL_EQ returns the theorem A |- (!x. t1) = (!x. t2), unless the variable x is free in any of the assumptions. 
         A |- t1 = t2
   ------------------------  FORALL_EQ "x"      [where x is not free in A]
    A |- (!x.t1) = (!x.t2)

FAILURE
Fails if the theorem is not an equation between boolean terms, or if the supplied term is not simply a variable, or if the variable is free in any of the assumptions.
SEEALSO
AP_TERM, EXISTS_EQ, SELECT_EQ
HOL  Kananaskis-13