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 /\ out = [Locked] /\ held st' = true)).
proof: Proof. Proof using. handler_unfold. intros. repeat break_match; repeat tuple_inversion; subst; auto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)