As terms now have types instead of sorts, the definition of well-sorted terms and formulas should be replaced with a definition of well-typed terms and formulas.
The rules for well-typedness are almost as before. Here, we will just mention those that are concerned with subtyping:
If T is a well-typed term of type t and t < => t', then T is also a well-typed term of type t'.
A term T of type t must only be casted to a type t', if t' < -> t.
A formula T e t is well-typed only if T is a well-typed term of type t' and t < => t'.