EQT_ELIM : (thm -> thm)
STRUCTURE
Drule
SYNOPSIS
Eliminates equality with T.
DESCRIPTION
    A |- tm = T
   -------------  EQT_ELIM
      A |- tm

FAILURE
Fails if the argument theorem is not of the form A |- tm = T.
SEEALSO
EQT_INTRO, EQF_ELIM, EQF_INTRO
HOL  Trindemossen-1