enrich
olist
with
functions
sort : List → List;
variables
x : List;
y : List;
z : List;
a : Elem;
b : Elem;
c : Elem;
axioms
Ordered: ordered≤(sort(x));
Perm: perm(x, sort(x));
end enrich