Implement new approach to proof of original variant

theories/logrel/F_mu_ref_conc/examples/queue/MS_queue_alt.v

@@ -88,7 +88,7 @@ Definition MS_enqueue :=
                       (* c = InjL ... Tail is nil, we can try to insert now *)
                       (If
                         (CAS (Var 2 (* c *)) (Var 1 (* t *)) (Var 5 (* n *)))
-                        (* Insertion succeeded, we are done *)
+                        (* Insertion succeeded *)
                         (Seq
                           (* Update the tail pointer *)
                           (Store (Var 8 (* tail *)) (Var 5 (* n *)))