Reduction, equality and unification are studied for a family of simply typed -calculi with subtypes. The subtype relation is required to relate base types only to base types and to satisfy some order-theoretic conditions. Constants are required to have a least type, i.e. no overloading. We define the usual and a subtype-dependent -reduction. These are related to a typed equality relation and shown to be confluent in a certain sense.