% $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