proposition: Lemma messages_trigger_labels : forall l p, message_enables_label p l -> message_delivered_label p l -> forall s, lb_step_execution lb_step_async s -> In p (nwPackets (evt_a (hd s))) -> weak_until (now (enabled lb_step_async l)) (now (occurred l)) s.
proof: Proof. Proof using. intros l p Henabled Hdelivered. cofix c. destruct s. destruct e. simpl. intros Hexec Hin. invcs Hexec. destruct (label_eq_dec l evt_l). - subst evt_l. apply W0. simpl. reflexivity. - apply W_tl. + simpl. unfold message_enables_label in *. unfold enabled. simpl. now auto. + simpl. apply c; auto. simpl. match goal with | |- In ?p ?ps => destruct (In_dec packet_eq_dec p ps) end; auto. unfold message_delivered_label in *. now find_apply_hyp_hyp. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)