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