EQT_ELIM : thm -> thm

SYNOPSIS

Eliminates equality with T.

DESCRIPTION

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

FAILURE CONDITIONS

Fails if the argument theorem is not of the form A |- tm <=> T.

EXAMPLE

  # REFL `T`;;
  val it : thm = |- T <=> T

  # EQT_ELIM it;;
  val it : thm = |- T

SEE ALSO

EQF_ELIM, EQF_INTRO, EQT_INTRO.