Def S T == x:S. x T
with the consquence that
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. S T (S List) (T List) A,A',B,B':Type. A A' B B' (A'B) (AB')
but these are not even well-formed propositions.
Similarly, there are properties about
Then we would be able to express properly theorems like
S,T:Type. S =ext T S List =ext T List S:Type, x:S, T:Type. S =ext T x T
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.
has worked out a suitable set of rules for the new subtype
relation which we need to incorporate into the standard