EQF_ELIM : (thm -> thm)
STRUCTURE
Drule
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
EQF_INTRO
,
EQT_ELIM
,
EQT_INTRO
HOL
Kananaskis-13