CONTR : term -> thm -> thm

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 CONDITIONS
Fails unless the term has type bool and the theorem has F as its conclusion.

EXAMPLE
  # let th = REWRITE_RULE[ARITH] (ASSUME `1 = 0`);;
  val th : thm = 1 = 0 |- F

  #  CONTR `Russell:Person = Pope` th;;
  val it : thm = 1 = 0 |- Russell = Pope

SEE ALSO
CCONTR, CONTR_TAC, NOT_ELIM.