(sorts s, t

sorts s, t < s; s, t < t

op g : s -> t

op g : s ->? s,[ forall v1 : s . def g(v1) ])