EQF_INTRO
Drule.EQF_INTRO : (thm -> thm)
Converts negation to equality with F.
A |- ~tm
------------- EQF_INTRO
A |- tm = F
Failure
Fails if the argument theorem is not a negation.
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