1\DOC EQF_ELIM
2
3\TYPE {EQF_ELIM : (thm -> thm)}
4
5\SYNOPSIS
6Replaces equality with {F} by negation.
7
8\KEYWORDS
9rule, negation, falsity.
10
11\DESCRIBE
12{
13    A |- tm = F
14   -------------  EQF_ELIM
15     A |- ~tm
16}
17
18
19\FAILURE
20Fails if the argument theorem is not of the form {A |- tm = F}.
21
22\SEEALSO
23Drule.EQF_INTRO, Drule.EQT_ELIM, Drule.EQT_INTRO.
24\ENDDOC
25