Unfold [transitivity] and [symmetry] in the corresponding tactics

Thanks, this is better.  Is the "symmetry is too smart for its own good" comment worth keeping, now that we're redefining `transitivity` as well?  If so, maybe it should be something like "Even if we weren't using [cbn], we would have to redefine `symmetry`, since the built-in Coq version is too smart for its own good."