EQT_INTRO : thm -> thm
STRUCTURE
Drule
SYNOPSIS
Introduces equality with T.
DESCRIPTION
      A |- tm
   -------------  EQT_INTRO
    A |- tm = T

FAILURE
Never fails.
SEEALSO
EQT_ELIM, EQF_ELIM, EQF_INTRO
HOL  Kananaskis-14