proposition: Lemma ClientNetHandler_lbcases : forall c m st l out st' ms, ClientNetHandler c m st = (l, out, st', ms) -> ms = [] /\ ((st' = st /\ out = [] /\ l = Nop) \/ (m = Locked /\ out = [Locked] /\ held st' = true /\ l = MsgLocked c)).
proof: Proof. Proof using. handler_unfold. intros. repeat break_match; repeat tuple_inversion; subst; intuition. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)