\DOC mk_eq

\TYPE {mk_eq : term * term -> term}

\SYNOPSIS
Constructs an equation.

\DESCRIBE
{mk_eq(t1, t2)} returns the term {t1 = t2}.

\FAILURE
Fails if the type of {t1} is not equal to that of {t2}.

\SEEALSO
boolSyntax.dest_eq, boolSyntax.is_eq.
\ENDDOC