EQ_IMP_RULE : thm -> thm * thm
A |- t1 <=> t2 ----------------------------------- EQ_IMP_RULE A |- t1 ==> t2 A |- t2 ==> t1
# SPEC_ALL CONJ_SYM;; val it : thm = |- t1 /\ t2 <=> t2 /\ t1 # EQ_IMP_RULE it;; val it : thm * thm = (|- t1 /\ t2 ==> t2 /\ t1, |- t2 /\ t1 ==> t1 /\ t2)