LP, the Larch Prover  Equality operators
LP automatically declares an equality operator = and an inequality operator
~= with signature S,S:>Bool for each sort S. These operators
have the standard interpretation: two objects of some sort S are equal if
and only if they are identical.
Operationally, LP uses equational termrewriting
to reduce a term t to a normal form t' such that the formula
t = t' is true. For this purpose, LP:

treats the equality operator as commutative except
when S is Bool, in which case LP treats it as a synonym for the
associativecommutative operator <=> for
logical equivalence.

uses two hardwired rewrite rules for each sort S
 x:S = x:S > true
 x:S ~= y:S > ~(x = y)

registers the operators = and ~= as
having multiset status for the purpose of
orienting formulas into rewrite rules.