equalities contains the declaration for =. It has a single type parameter. Properties of equality are given in equality_props.
equalities [T:TYPE] : THEORY BEGIN
=: [T, T- > boolean] ; END equalities