----------------------------------------------------------------------
CONTRAPOS                                                      (Drule)
----------------------------------------------------------------------
CONTRAPOS : (thm -> thm)

SYNOPSIS
Deduces the contrapositive of an implication.

KEYWORDS
rule, contrapositive, implication.

DESCRIBE
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
Thm.CCONTR, Drule.CONTR, Conv.CONTRAPOS_CONV, Thm.NOT_ELIM.

----------------------------------------------------------------------