If M is the term t1 = t2, then dest_eq_ty M returns
(t1, t2, ty), where ty is the type of t1 (and thus also of
t2).
FAILURE
Fails if M is not an equality.
USES
Gives an efficient way to break apart an equality and get the
type of the equality. Useful for obtaining that last fraction of speed
when optimizing the bejeesus out of an inference rule.