module type EQUATION =`sig`

..`end`

`type `

t

`type `

rhs

An equation can have something other than a term as a right-hand
side, for instance a formula.

`val compare : ``t -> t -> int`

Total order on equations

`val extract : ``t -> LogtkIndex.term * rhs * bool`

Obtain a representation of the (in)equation. The sign indicates
whether it is an equation

`l = r`

(if true) or an inequation
`l != r`

(if false)`val priority : ``t -> int`

How "useful" this equation is. Can be safely ignored by
always returning the same number.