CONJ_PAIR

Drule.CONJ_PAIR : thm -> thm * thm

Extracts both conjuncts of a conjunction.

       A |- t1 /\ t2
   ----------------------  CONJ_PAIR
    A |- t1      A |- t2

The two resultant theorems are returned as a pair.

Failure

Fails if the input theorem is not a conjunction.

See also

Drule.BODY_CONJUNCTS, Thm.CONJUNCT1, Thm.CONJUNCT2, Thm.CONJ, Drule.LIST_CONJ, Drule.CONJ_LIST, Drule.CONJUNCTS