This aspect introduces a subtype predicate that can reference ghost entities. The subtype cannot appear as a subtype_mark in a membership test.
For the detailed semantics of this aspect, see the entry for subtype predicates in the SPARK Reference Manual, section 3.2.4.