A cast term is written:

T as S

It is well-sorted if the term T is well-sorted for a supersort S' of S. It expands to an application of the pre-declared operation symbol for projecting from S' to S.

Term formation is also extended by letting a well-sorted term of a subsort S be regarded as a well-sorted term of a supersort S' as well, which provides implicit embedding. It expands to the explicit application of the pre-declared operation symbol for embedding S into S'. (There are no implicit projections.) Also a sorted-term T:S' expands to an explicit application of an embedding, provided that the apparent sort S of the component term T is a subsort of the specified sort S'.