We extend the framework of Pure Type Systems with subtyping, as found in
F-omega-sub. This leads to a concise description of many existing systems
with subtyping, and also to some new interesting systems. We develop the
meta-theory for this framework, including Subject Reduction and Minimal Typing.

The main problem was how to formulate the rules of the framework in such a way
that we avoid circularities between theory about typing and theory about
subtyping. We solve this problem by a simple but rigorous design decision:
the subtyping rules do not depend on the typing rules.