mk_eq : term * term -> term
STRUCTURE
SYNOPSIS
Constructs an equation.
DESCRIPTION
mk_eq(t1, t2) returns the term t1 = t2.
FAILURE
Fails if the type of t1 is not equal to that of t2.
SEEALSO
HOL  Kananaskis-14