EQF_ELIM : thm -> thm

SYNOPSIS

Replaces equality with F by negation.

DESCRIPTION

    A |- tm <=> F
   ---------------  EQF_ELIM
     A |- ~tm

FAILURE CONDITIONS

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

EXAMPLE

  # EQF_ELIM(REFL `F`);;
  val it : thm = |- ~F

SEE ALSO

EQF_INTRO, EQT_ELIM, EQT_INTRO, NOT_ELIM, NOT_INTRO.