proposition: Lemma Locked_delivered_MsgLocked : forall i, message_delivered_label {| pSrc := Server; pDst := Client i; pBody := Locked |} (MsgLocked i).
proof: Proof. Proof using. unfold message_delivered_label. intros. invcs H. - repeat find_rewrite. find_eapply_lem_hyp In_split_not_In; eauto. subst. monad_unfold. simpl in *. handler_unfold. repeat break_match; repeat find_inversion; auto. - unfold not in *. find_false. apply in_app_iff; auto. - intuition. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)