 The type-assignment system TA\(_\textrm{CL}\) is formally defined as the following deduction system. (When implicational formulas are considered as types, the usual convention is to omit parentheses by association to the right.)