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