ADT AddNEQ [T]
/* This is a trivial example, it just extends type T with 
   a not-equal predicate */

INITIALS

CONSTRUCTORS

SELECTORS
  NEQ: T*T->BOOL

AXIOMS

  NEQ(x,y)=NOT(EQUAL(x,y))