CONTR
Drule.CONTR : term -> thm -> thm
Implements the intuitionistic contradiction rule.
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.