Recovering the companion's "symmetric" tactic in the heterogeneous branch

[YaZko]

The coq-coinduction library provides a quite convenient tactic to leverage symmetry arguments in bisimulation proofs, avoiding to repeat the proof essentially to the identical in each direction.
The tactic is however quite strongly tied to the syntactic definition of a bisimulation as the intersection of a simulation and its reverse, which we lost when we generalized things to the heterogenous.
Can we recover it nicely in the cases where the proof method holds nonetheless?

[nchappe]

f324ee9 recovers it in the case of sbisim eq. I guess it could be generalized for any homogeneous equivalence relation, but the relevant typeclass of coq-coinduction is probably not enough for heterogeneous relations.