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

FAILURE
Never fails.
SEEALSO
HOL  Kananaskis-14