EQT_INTRO : thm -> thm

SYNOPSIS

Introduces equality with T.

DESCRIPTION

      A |- tm
   ---------------  EQF_INTRO
    A |- tm <=> T

FAILURE CONDITIONS

Never fails.

EXAMPLE

  # EQT_INTRO (REFL `2`);;
  val it : thm = |- 2 = 2 <=> T

SEE ALSO

EQF_ELIM, EQF_INTRO, EQT_ELIM.