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