CONJ_TAC : tactic
Reduces a conjunctive goal to two separate subgoals.
When applied to a goal
A ?- t1 /\ t2
, the tactic
reduces it to the two subgoals corresponding to each conjunct separately.
A ?- t1 /\ t2 ====================== CONJ_TAC A ?- t1 A ?- t2
Fails unless the conclusion of the goal is a conjunction.