mk_conj : term * term -> term
STRUCTURE
SYNOPSIS
Constructs a conjunction.
DESCRIPTION
mk_conj(t1, t2) returns the term t1 /\ t2.
FAILURE
Fails if t1 and t2 do not both have type bool.
SEEALSO
HOL  Kananaskis-14