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

Just to clarify, this trick would get rid of the constant `symmetric_paths`, but not the constant `symmetry`, right?  So it wouldn't eliminate the need for the fancier tactics if we want to be able to write `symmetry` and get out a term containing `inverse` rather than `symmetry`?