CONTRAPOS : (thm -> thm)
STRUCTURE
Drule
SYNOPSIS
Deduces the contrapositive of an implication.
DESCRIPTION
When applied to a theorem A |- s ==> t, the inference rule CONTRAPOS returns its contrapositive, A |- ~t ==> ~s. 
     A |- s ==> t
   ----------------  CONTRAPOS
    A |- ~t ==> ~s

FAILURE
Fails unless the theorem is an implication.
SEEALSO
CCONTR, CONTR, CONTRAPOS_CONV, NOT_ELIM
HOL  Kananaskis-13