Log Message: 
1. Replaced equality relations with equivalence relations in
the definition axioms for "op", "inv", and "id".
2. Defined the equivalence functionality for "op" and "inv".
3. Changed the tactics for "left and right cancellation laws"
(i.e., groupCancelLeftT and groupCancelRightT) to make it
easier to use.
4. Reproved all properties.
