This paper presents two definitions of the subtype relation in object-oriented programming, both of which ensure that any property proved about supertype objects also holds for their subtype objects. The first definition, called the constraint rule, requires that the history properties of a subtype are explicitly stated in its specification. The second definition, called the extension map, allows extra methods of a subtype to be explained in terms of existing methods of the supertype. Both definitions ensure that the behavior of subtypes is consistent with the behavior of supertypes, and that properties such as invariants and history properties are preserved. The paper also discusses the implications of these definitions for the design of type families, and provides examples to illustrate the concepts. The first definition is based on the idea that the history properties of a subtype must be compatible with those of the supertype, while the second definition allows for more flexibility by explaining the behavior of extra methods in terms of existing methods. The paper concludes that both definitions are effective in ensuring that subtypes behave correctly with respect to supertypes.This paper presents two definitions of the subtype relation in object-oriented programming, both of which ensure that any property proved about supertype objects also holds for their subtype objects. The first definition, called the constraint rule, requires that the history properties of a subtype are explicitly stated in its specification. The second definition, called the extension map, allows extra methods of a subtype to be explained in terms of existing methods of the supertype. Both definitions ensure that the behavior of subtypes is consistent with the behavior of supertypes, and that properties such as invariants and history properties are preserved. The paper also discusses the implications of these definitions for the design of type families, and provides examples to illustrate the concepts. The first definition is based on the idea that the history properties of a subtype must be compatible with those of the supertype, while the second definition allows for more flexibility by explaining the behavior of extra methods in terms of existing methods. The paper concludes that both definitions are effective in ensuring that subtypes behave correctly with respect to supertypes.