proposition: Lemma message_labels_eventually_occur : forall l p, l <> label_silent -> message_enables_label p l -> message_delivered_label p l -> forall s, weak_fairness lb_step_async label_silent s -> lb_step_execution lb_step_async s -> In p (nwPackets (evt_a (hd s))) -> eventually (now (occurred l)) s.
proof: Proof. Proof using. intros. find_eapply_lem_hyp messages_trigger_labels; eauto. find_apply_lem_hyp weak_until_until_or_always. intuition. - now eauto using until_eventually. - find_apply_lem_hyp always_continuously. eapply_prop_hyp weak_fairness continuously; auto. destruct s. now find_apply_lem_hyp always_now. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)