EQT_ELIM : (thm -> thm)
STRUCTURE
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
HOL  Trindemossen-1