¹¹  Such textual substitutivity is central to the tractability of not only our type description language but also other type description languages in general.