CONTRAPOS_CONV : term -> thm
Proves the equivalence of an implication and its contrapositive.
When applied to an implication `p ==> q`, the conversion CONTRAPOS_CONV
returns the theorem:
|- (p ==> q) <=> (~q ==> ~p)
- FAILURE CONDITIONS
Fails if applied to a term that is not an implication.
The same effect can be had by GEN_REWRITE_CONV I [GSYM CONTRAPOS_THM]
- SEE ALSO