EQF_ELIM : (thm -> thm)
STRUCTURE
SYNOPSIS
Replaces equality with F by negation.
DESCRIPTION
    A |- tm = F
   -------------  EQF_ELIM
     A |- ~tm

FAILURE
Fails if the argument theorem is not of the form A |- tm = F.
SEEALSO
HOL  Trindemossen-1