EQT_ELIM
Drule.EQT_ELIM : (thm -> thm)
Eliminates equality with T.
A |- tm = T
------------- EQT_ELIM
A |- tm
Failure
Fails if the argument theorem is not of the form A |- tm = T.
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