IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

The Subtyping Relation between Types

AB is a proposition for any types A and B, and is true just when A is a subtype of B.

As indicated in Subtype Relation, the standard set of primitive operators has not included a notation for the two-place relation of subtyping between two types. In advance of it adoption for normal development, some users have forged ahead with its incorporation, though tactic support is still not adequate for the typical user. The operator is AB. It differs from AB in its well-formedness conditions. While AB is a well formed proposition only when it is true, and so is useless as the antecedent of an implication, AB is a well formed proposition so long as A and B are type expressions, independently of whether A really is a subtype of B. (On the other hand, AB is well formed if A denotes the empty type no matter whether B denotes a type.)