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.

SEE ALSO

is_imp, mk_imp, strip_imp.