CONTRAPOS_CONV : conv
STRUCTURE
SYNOPSIS
Proves the equivalence of an implication and its contrapositive.
DESCRIPTION
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
HOL  Kananaskis-14