Conjoins multiple assumptions to both sides of an equation.
DESCRIPTION
Given a term list [t1;...;tn] and a theorem whose conclusion is an equation
between boolean terms, CONJ_DISCHL conjoins all the terms
in the list to both sides of the equation, and removes any of the terms which
were in the assumption list.
A |- s = t
-------------------------------------------------------- CONJ_DISCHL
A - {t1,...,tn} |- (t1/\.../\tn/\s) = (t1/\.../\tn/\t) [t1,...,tn]
FAILURE
Fails unless the theorem is an equation, both sides of which, and all the terms
provided, are of type bool.