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