Equality (T):[Table of Contents] [Index]trait% This trait is given for documentation only. % It is implicit in LSL.introduces__ = __, __ \neq __: T, T -> BoolassertsTpartitionedby=forallx, y, z: T x = x; x = y == y = x; (x = y /\ y = z) => x = z; x \neq y == ~(x = y)impliesEquivalence (=for\equiv)