dest_imp : term -> term * term

SYNOPSIS
Breaks apart an implication into antecedent and consequent.

DESCRIPTION
dest_imp is a term destructor for implications. Thus
   dest_imp `t1 ==> t2`
returns
   (`t1`,`t2`)

FAILURE CONDITIONS
Fails with dest_imp if term is not an implication.

COMMENTS
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.