% $Id$

Function(F, D, R): trait
% LSL relation and function traits are over-specified:
% they assume domain and range are the same sort.
  introduces
    __ [__] : F, D -> R

  asserts forall f:F, x:D, y,z: R
    f[x] = y /\ f[x] = z => y = z