dest_eq : term -> term * term

SYNOPSIS
Term destructor for equality.

DESCRIPTION
dest_eq(`t1 = t2`) returns (`t1`,`t2`).

FAILURE CONDITIONS
Fails with dest_eq if term is not an equality.

EXAMPLE
  # dest_eq `2 + 2 = 4`;;
  val it : term * term = (`2 + 2`, `4`)

SEE ALSO
is_eq, mk_eq.