EQF_INTRO : (thm -> thm)
STRUCTURE
SYNOPSIS
Converts negation to equality with F.
DESCRIPTION
     A |- ~tm
   -------------  EQF_INTRO
    A |- tm = F

FAILURE
Fails if the argument theorem is not a negation.
SEEALSO
HOL  Trindemossen-1