dest_imp : term -> term * term
Breaks apart an implication into antecedent and consequent.
dest_imp is a term destructor for implications. Thus
- FAILURE CONDITIONS
Fails with dest_imp if term is not an implication.
Previous version of dest_imp treats negations as an implication
with F as the conclusion. This is renamed to dest_neg_imp.
- SEE ALSO
mk_imp, is_imp, strip_imp, dest_neg_imp.