Add the definition of Constraint Typing Relation.
Add the definition of solution for the (Gamma, t, S, C).