CONTR : term -> thm -> thm
STRUCTURE
Drule
SYNOPSIS
Implements the intuitionistic contradiction rule.
DESCRIPTION
When applied to a term t and a theorem A |- F, the inference rule CONTR returns the theorem A |- t. 
    A |- F
   --------  CONTR t
    A |- t

FAILURE
Fails unless the term has type bool and the theorem has F as its conclusion.
SEEALSO
CCONTR, CONTRAPOS, CONTR_TAC, NOT_ELIM
HOL  Trindemossen-1