 Principal types and principal type schemas may seem now to be interchangeable everywhere. Thus we could take a slightly different approach and define \(\textrm{TA}_\textrm{CL}\) to include axioms and the rule schema of detachment together with the rule of substitution. This version of \(\textrm{TA}_\textrm{CL}\) would assume the following form.