feat: Bisimilarity can be characterized through symmetric simulation relations

[benkeks]

In formalized proofs, the characterization of bisimilarity through symmetric simulations often is more convenient than the one through bisimulation relations. (The reason is that paper proofs about bisimulation often say “the converse case is analogous,” which is not possible in proof assistants. The background usually is that the witness simulation is symmetric or can easily be adapted to be symmetric, which can usually be handled conveniently in a proof assistant.)

Being about alternative characterizations of bisimilarity notions, the PR also proposes to remove the SWBisimilarity relation and only see SWBisimulation as an alternative characterization mechanism for WeakBisimilarity. The thought behind this is that there usually are many ways of characterizing the same notion of equivalence. Especially the weak spectrum has rich aliasing of notions, e.g. with a range of different definitions all leading to the same branching bisimilarity relation. It seems impractical to grant each equivalent definition its own relation symbol.

Also, some proofs are shortened a bit using grind.

[fmontesi]

Very nice, thanks! I just have a couple of minor comments.