 The first axiom and the first two rules constitute equational logic. The constants are again the combinators \(\textsf{S}\) and \(\textsf{K}\). Note that \(\text{CL}_=\) could have been defined as an extension of \(\text{CL}_\triangleright\) by adding the rule of symmetry, that would have paralleled the description of the definition of equality from reduction as its transitive, symmetric closure. We chose instead to repeat the inequational axioms and rules with the new notation (and add the rule of symmetry) to make the two definitions self-contained and easy to grasp. The two characterizations of \(=\) coincide—as those of \(\triangleright\) did.