Reduces a conjunctive goal to two subgoals: prove the first conjunct assuming
the second, then prove the second conjunct.
DESCRIPTION
When applied to a goal A ?- t1 /\ t2, the tactic CONJ_ASM2_TAC reduces it
to two subgoals corresponding to the two conjuncts, assuming the first to
prove the second.
A ?- t1 /\ t2
========================== CONJ_ASM2_TAC
A u {t2} ?- t1 A ?- t2
FAILURE
Fails unless the conclusion of the goal is a conjunction.