When applied to a contradictory theorem A' |- F, and a goal A ?- t,
the tactic CONTR_TAC completely solves the goal. This is an invalid
tactic unless A' is a subset of A.
A ?- t
======== CONTR_TAC (A' |- F)
FAILURE
Fails unless the theorem is contradictory, i.e. has F as its conclusion.