CONJ_ASM2_TAC
Tactic.CONJ_ASM2_TAC : tactic
Reduces a conjunctive goal to two subgoals: prove the first conjunct assuming the second, then prove the second conjunct.
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.