proposition: Lemma MsgLock_Locked : forall c s, event_step_star step_async step_async_init (hd s) -> lb_step_execution lb_step_async s -> weak_fairness lb_step_async label_silent s -> now (occurred (MsgLock c)) s -> eventually (fun s => In (mkPacket Server (Client c) Locked) (nwPackets (evt_a (hd s)))) s.
proof: Proof. Proof using. intros. find_apply_lem_hyp MsgLock_in_queue_or_Locked; auto. intuition. - destruct s; simpl in *; eauto using E_next, E0. - break_exists. destruct s; simpl in *. apply E_next. eapply clients_get_lock_messages; eauto using lb_step_execution_invar, weak_fairness_invar. find_apply_lem_hyp step_async_star_lb_step_execution; auto. destruct s. simpl. do 2 (find_apply_lem_hyp always_Cons; intuition). Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)