System F !<= is an extension with subtyping of Girard's higher-order polymorphic >=-calculus. We develop
the fundamental metatheory of this calculus: decidability of -conversion on well-kinded types, elimination
of the \cut-rule" of transitivity from the subtype relation, and the soundness, completeness, and
termination of algorithms for subtyping and typechecking.