WIP: Add Michael Scott queue

Adds an additional example: A proof that the Michael-Scott queue, and a variant of it, is a refinement of a course-grained queue.

As of right now the proofs use the lemmas refines_load_alt and refines_cmpxchg_l_alt, as the refines_load and refines_cmpxchg_l in ReLoC are not strong enough. Before merging the MR I think it would make sense to decide what the best solution to that is. Should those lemmas or variants of them be added to ReLoc? Should the existing lemmas be changed? Or something else?

I've marked the MR WIP as I'll also submit a MR for iris/examples with a version of the proof that I did without using ReLoC.