Since term is an ML eqtype, any two terms tm1 and tm2
can be tested for equality by tm1 = tm2. However, the fundamental
notion of equality for terms is implemented by aconv.
Since term is an abstract type, access to its representation is mediated
by the interface presented by the Term structure.