Symbol of the function that computes coercions. Coercion rules are added on that symbol.

apply a b t creates the coercion of term t from type a to type b.