proposition: Lemma Lock_in_network_eventually_MsgLock : forall c s, lb_step_execution lb_step_async s -> weak_fairness lb_step_async label_silent s -> In (mkPacket (Client c) Server Lock) (nwPackets (evt_a (hd s))) -> eventually (now (occurred (MsgLock c))) s.
proof: Proof. Proof using. intros. eapply message_labels_eventually_occur; eauto using Lock_enables_MsgLock, Lock_delivered_MsgLock. unfold label_silent. simpl. congruence. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)