with the consquence that ST does not express a general relation between types (even restricted to a Universe). This is because, as explained in Equality, "tT" is assigned a meaning only when it is true, and therefore also ST is assigned a meaning only when
it is true. Thus, it is not true that "S,T:Type. ST Prop", and so one cannot effectively use ST as an assumption is propositions.

This is quite unfortunate since there are many natural properties we would like to state about a subtyping relation between types, such as

S,T:Type. ST (S List) (T List)

A,A',B,B':Type. AA'BB' (A'B) (AB')

but these are not even well-formed propositions.
Similarly, there are properties about extensional equality between types that we would like to express, and we would be able to once we defined an extensional equality
relation in Nuprl as symmetric closure of subtyping.
Then we would be able to express properly theorems like

S,T:Type. S =ext TS List =ext T List

S:Type, x:S, T:Type. S =ext TxT

which would be quite handy as lemmas.

A better approach, which we intend to adopt later, is to add a new primitive operator that is stipulated to be well formed whenever its two arguments are types, and is true just when the one type is in fact a subtype of the other, i.e., when every pair of terms equal in the first type are also equal in the second.

Note that these two concepts can technically coexist, so extant theorems using the old form of subtyping would survive.
Karl Crary
has worked out a suitable set of rules for the new subtype
relation which we need to incorporate into the standard tactics.