proposition: Lemma Locked_enables_MsgLocked : forall i, message_enables_label {| pSrc := Server; pDst := Client i; pBody := Locked |} (MsgLocked i).
proof: Proof. Proof using. unfold message_enables_label, enabled. intros. find_apply_lem_hyp in_split. break_exists_name xs. break_exists_name ys. do 2 eexists. eapply LabeledStepAsync_deliver; eauto. simpl. monad_unfold. simpl. eauto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)