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)
USES
One quite common pattern is to use a contradictory hypothesis via
FIRST_ASSUM CONTR_TAC.
FAILURE CONDITIONS
Fails unless the theorem is contradictory, i.e. has F as its conclusion.