CONTRAPOS_CONV : conv
STRUCTURE
Conv
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
CONTRAPOS
HOL
Kananaskis-10