CONTRAPOS : (thm -> thm)
STRUCTURE
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
HOL  Trindemossen-1