s/R/B in ≈-coind.
Removed an unproven conjecture.
Simplified some proofs by using a trivial bisimulation.