EQF_ELIM
Drule.EQF_ELIM : (thm -> thm)
Replaces equality with F by negation.
A |- tm = F
------------- EQF_ELIM
A |- ~tm
Failure
Fails if the argument theorem is not of the form A |- tm = F.
Press ← or → to navigate between chapters
Press S or / to search in the book
Press ? to show this help
Press Esc to hide this help