proposition: Lemma Lock_enables_MsgLock : forall i, message_enables_label (mkPacket (Client i) Server Lock) (MsgLock i).
proof: Proof. Proof using. unfold message_enables_label. intros. find_apply_lem_hyp in_split. break_exists_name xs. break_exists_name ys. unfold enabled. destruct (ServerNetHandler (Client i) Lock (nwState net Server)) eqn:?. destruct p. destruct p. cut (l0 = MsgLock i); intros. subst. - repeat eexists. econstructor; eauto. - handler_unfold. repeat break_match; repeat find_inversion; auto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)