proposition: Lemma InputLock_eventually_MsgLock : forall c s, lb_step_execution lb_step_async s -> weak_fairness lb_step_async label_silent s -> now (occurred (InputLock c)) s -> eventually (now (occurred (MsgLock c))) s.
proof: Proof. Proof using. intros. find_apply_lem_hyp InputLock_Lock; auto. destruct s. simpl in *. eauto using E_next, Lock_in_network_eventually_MsgLock, lb_step_execution_invar, weak_fairness_invar. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)