----------------------------------------------------------------------
CONTRAPOS_CONV                                                  (Conv)
----------------------------------------------------------------------
CONTRAPOS_CONV : conv

SYNOPSIS
Proves the equivalence of an implication and its contrapositive.

KEYWORDS
conversion, contrapositive, implication.

DESCRIBE
When applied to an implication {P ==> Q}, the conversion {CONTRAPOS_CONV}
returns the theorem:

   |- (P ==> Q) = (~Q ==> ~P)




FAILURE
Fails if applied to a term that is not an implication.

SEEALSO
Drule.CONTRAPOS.

----------------------------------------------------------------------