Restriction: The two <term>s in an equation must have the same sort. This
sort must be Bool if the equality operator is <=>.

Examples

x + 0 = x
x <= y <=> x < y \/ x = y
x | y <=> \E z (y = x*z)

Usage

LP treats equations in the same manner as it treats formulas. Indeed, any
formula is logically equivalent to an equation: F is logically equivalent
to F <=> true.