Description: Show the commutative law for an operation O on a toy structure class
C of commuatitive operations on CC . This illustrates how a
structure class can be partially specialized. In practice, we would
ordinarily define a new constant such as "CAbel" in place of C .
(Contributed by NM, 17-Mar-2013)(Proof modification is discouraged.)