WIP: MS-queue

This MR adds an additional example to the logrel development: A proof that the Michael-Scott queue, and a variant of it, is a refinement of a course-grained queue.

I've marked the MR WIP as it, at least, needs to be updated with a link to the accompanying notes (they are not hosted anywhere yet, but a draft is here). Additionally, I have an MR with the same proof, but based on ReLoC, here and any feedback on one is probably also applicable to the other.

The MR also makes a few small changes to some of the existing examples better adapting them to changes that have happened in Iris.