CONJ_PAIR : thm -> thm * thm
A |- t1 /\ t2 ---------------------- CONJ_PAIR A |- t1 A |- t2
# CONJ_PAIR(ASSUME `p /\ q`);; val it : thm * thm = (p /\ q |- p, p /\ q |- q)