is_imp : term -> bool

SYNOPSIS: Tests if a term is an application of implication.
DESCRIPTION: The call is_imp t returns true if t is of the form p ==> q for some p and q, and returns false otherwise.
FAILURE CONDITIONS: Never fails.
SEE ALSO: dest_imp.