EQF_INTRO : thm -> thm

SYNOPSIS

Converts negation to equality with F.

DESCRIPTION

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

FAILURE CONDITIONS

Fails if the argument theorem is not a negation.

EXAMPLE

  # let th = ASSUME `~p`;;
  val th : thm = ~p |- ~p

  # EQF_INTRO th;;
  val it : thm = ~p |- p <=> F

SEE ALSO

EQF_ELIM, EQT_ELIM, EQT_INTRO, NOT_ELIM, NOT_INTRO.