May variables be overloaded, i.e. can a set of sorted variables X contain x:s and x:s' with s /= s'? Probably not, since things like forall x:s. forall x:s'. f(x)=x for f : s -> s' might be confusing. But what about examples like
orvar x:s ... ... axiom forall x:s'. phi
If overloading is forbidden, these could still be allowed if overriding is permitted: later declarations supercede earlier ones. Then forall x:s. forall x:s'. f(x)=x would only be well-formed if f : s' -> s'.var x:s ... ... var x:s'