dest_eq : term -> term * term
STRUCTURE
SYNOPSIS
Term destructor for equality.
DESCRIPTION
If M is the term t1 = t2, then dest_eq M returns (t1, t2).
FAILURE
Fails if M is not an equality.
SEEALSO
HOL  Trindemossen-1